Extended continuants and bi-infinite continued fractions

DefinitionForward branch of the extended continuant#✓fully proved

For an integer sequence \(x : \mathbb{Z} \to \mathbb{Z}\) and an integer \(b\), the forward branch with start index \(b\) is the sequence \((F_n)_{n \ge 0}\) of integers defined by \(F_0 = 0\), \(F_1 = 1\) and \(F_{n+2} = x_{b+n} F_{n+1} + F_n\). Its value \(F_n\) is the extended continuant \(K_{n-2}(x)_b\).

public def extendedContinuantFwd (x : ℤ → ℤ) (b : ℤ) : ℕ → ℤ
  | 0 => 0
  | 1 => 1
  | n + 2 => x (b + n) * extendedContinuantFwd x b (n + 1) + extendedContinuantFwd x b n
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Definition 3 (right-adjusting recurrence).
Used by 5
Used byExtended continuants · Extended continuant of order \(-1\) · Extended continuants of order \(-2\) vanish · Recurrence for extended continuants · The extended continuant of order \(0\) is a single term

DefinitionBackward branch of the extended continuant#✓fully proved

For an integer sequence \(x : \mathbb{Z} \to \mathbb{Z}\) and an integer \(b\), the backward branch with start index \(b\) is the sequence \((B_m)_{m \ge 0}\) of integers defined by \(B_0 = 1\), \(B_1 = 0\) and \(B_{m+2} = -x_{b-1-m} B_{m+1} + B_m\). Its value \(B_m\) is the extended continuant \(K_{-1-m}(x)_b\) of negative order \(-1-m\).

public def extendedContinuantBwd (x : ℤ → ℤ) (b : ℤ) : ℕ → ℤ
  | 0 => 1
  | 1 => 0
  | m + 2 => -x (b - 1 - m) * extendedContinuantBwd x b (m + 1) + extendedContinuantBwd x b m
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Definition 4 (right-adjusting recurrence).
Used by 5
Used byExtended continuants · Extended continuant of order \(-1\) · Extended continuants of order \(-2\) vanish · Recurrence for extended continuants · The extended continuant of order \(0\) is a single term

DefinitionExtended continuants#✓fully proved

Let \(x : \mathbb{Z} \to \mathbb{Z}\) be a bi-infinite integer sequence and \(b\) an integer. The extended continuant \(K_a(x)_b\) of order \(a \in \mathbb{Z}\) with start index \(b\) (the paper's \(K_a(x)_b^{a+b}\)) is the integer defined by \(K_{-2}(x)_b = 0\), \(K_{-1}(x)_b = 1\), the forward recurrence \(K_a(x)_b = x_{b+a} K_{a-1}(x)_b + K_{a-2}(x)_b\) for \(a \ge 0\), and the backward recurrence \(K_a(x)_b = K_{a+2}(x)_b - x_{b+a+2} K_{a+1}(x)_b\) for \(a \le -3\).

public def extendedContinuant (x : ℤ → ℤ) (a b : ℤ) : ℤ :=
  if 0 ≤ a + 2 then extendedContinuantFwd x b (a + 2).toNat
  else extendedContinuantBwd x b (-1 - a).toNat
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Definitions 3 and 4.
Uses 2 · Used by 17
Statement usesBackward branch of the extended continuant · Forward branch of the extended continuant
Used byBennett's continuant identity for all integer indices · Bennett's continuant identity for nonnegative indices · Determinant identity for extended continuants · Euler's continuant identity for extended continuants · Extended continuant of order \(-1\) · Reflection formula for the order of extended continuants · Extended continuants of orders \(-3\) to \(-6\) · Extended continuants of order \(-2\) vanish · Recurrence for extended continuants · Westbound matrix product of extended continuants · The extended continuant of order \(0\) is a single term · No silent sequences of even order · Terms of a \(\sigma\)-silent sequence for odd \(\sigma \ge 5\) · Terms of a \(1\)-silent sequence · Silent-term formulas on table (33), case \(\sigma \equiv 5 \pmod 6\) · Silent-term formulas on table (33), case \(\sigma \equiv 1 \pmod 6\) · Terms of 3-silent sequences

TheoremExtended continuants of order \(-2\) vanish#✓fully proved

For every bi-infinite integer sequence \(x : \mathbb{Z} \to \mathbb{Z}\) and every integer \(b\), the extended continuant of order \(-2\) with start index \(b\) is zero: \(K_{-2}(x)_b = 0\).

public theorem extendedContinuant_neg_two (x : ℤ → ℤ) (b : ℤ) :
    extendedContinuant x (-2) b = 0
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Definitions 3 and 4.
Uses 3 · Used by 1
Statement usesExtended continuants
Proof usesBackward branch of the extended continuant · Forward branch of the extended continuant
Used byExtended continuants of orders \(-3\) to \(-6\)

TheoremExtended continuant of order \(-1\)#✓fully proved

For every integer sequence \(x : \mathbb{Z} \to \mathbb{Z}\) and every integer \(b\), the extended continuant of \(x\) of order \(-1\) with start index \(b\) equals \(1\), that is, \(K_{-1}(x)_b = 1\).

public theorem extendedContinuant_neg_one (x : ℤ → ℤ) (b : ℤ) :
    extendedContinuant x (-1) b = 1
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Definitions 3 and 4.
Uses 3 · Used by 1
Statement usesExtended continuants
Proof usesBackward branch of the extended continuant · Forward branch of the extended continuant
Used byExtended continuants of orders \(-3\) to \(-6\)

TheoremThe extended continuant of order \(0\) is a single term#✓fully proved

For every bi-infinite integer sequence \(x : \mathbb{Z} \to \mathbb{Z}\) and every integer \(b\), the extended continuant of order \(0\) with start index \(b\) is \(K_0(x)_b = x_b\).

public theorem extendedContinuant_zero (x : ℤ → ℤ) (b : ℤ) :
    extendedContinuant x 0 b = x b
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Section 3.4 and Equation (13).
Uses 3
Statement usesExtended continuants
Proof usesBackward branch of the extended continuant · Forward branch of the extended continuant

TheoremRecurrence for extended continuants#✓fully proved

For every bi-infinite integer sequence \(x : \mathbb{Z} \to \mathbb{Z}\) and all integers \(a\) and \(b\), the extended continuants \(K_a(x)_b\) of order \(a\) with start index \(b\) satisfy \(K_a(x)_b = x_{b+a} K_{a-1}(x)_b + K_{a-2}(x)_b\).

For \(a \le -1\) this is the paper's backward recurrence of Definition 4.

public theorem extendedContinuant_recurrence (x : ℤ → ℤ) (a b : ℤ) :
    extendedContinuant x a b =
      x (b + a) * extendedContinuant x (a - 1) b + extendedContinuant x (a - 2) b
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Definitions 3 and 4 (RA versions).
Uses 3 · Used by 1
Statement usesExtended continuants
Proof usesBackward branch of the extended continuant · Forward branch of the extended continuant
Used byExtended continuants of orders \(-3\) to \(-6\)

TheoremExtended continuants of orders \(-3\) to \(-6\)#✓fully proved

Let \(x : \mathbb{Z} \to \mathbb{Z}\) be an integer sequence and write \(K_a(x)_b\) for its extended continuant of order \(a\) with start index \(b\). For every integer \(h\), \(K_{-3}(x)_h = 1\), \(K_{-4}(x)_h = -x_{h-2}\), \(K_{-5}(x)_h = 1 + x_{h-3} x_{h-2}\) and \(K_{-6}(x)_h = -(x_{h-4} + x_{h-2} + x_{h-4} x_{h-3} x_{h-2})\).

public theorem extendedContinuant_neg_three_to_six (x : ℤ → ℤ) (h : ℤ) :
    extendedContinuant x (-3) h = 1 ∧ extendedContinuant x (-4) h = -x (h - 2) ∧
      extendedContinuant x (-5) h = 1 + x (h - 3) * x (h - 2) ∧
      extendedContinuant x (-6) h = -(x (h - 4) + x (h - 2) + x (h - 4) * x (h - 3) * x (h - 2))
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Lemma 1.
Uses 4
Statement usesExtended continuants
Proof usesExtended continuant of order \(-1\) · Extended continuants of order \(-2\) vanish · Recurrence for extended continuants

TheoremWestbound matrix product of extended continuants#●ready to prove

Let \(x : \mathbb{Z} \to \mathbb{Z}\) be a bi-infinite integer sequence, write \(K_a(x)_b\) for the extended continuant of order \(a\) with start index \(b\), and put \(M_i = \begin{pmatrix} 0 & 1 \\ 1 & -x_{-i} \end{pmatrix}\). Then for every integer \(n \ge 1\),

\[ M_n M_{n-1} \cdots M_1 = \begin{pmatrix} K_{-n-1}(x)_0 & K_{-n-2}(x)_1 \\ K_{-n-2}(x)_0 & K_{-n-3}(x)_1 \end{pmatrix}. \]
public theorem_wanted extendedContinuant_westbound_matrix_prod (x : ℤ → ℤ) (n : ℕ)
    (hn : 1 ≤ n) :
    (List.ofFn fun i : Fin n => !![0, 1; 1, -x (-((n : ℤ) - i))]).prod =
      !![extendedContinuant x (-n - 1) 0, extendedContinuant x (-n - 2) 1;
        extendedContinuant x (-n - 2) 0, extendedContinuant x (-n - 3) 1]
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Proposition 1.
Uses 1
Statement usesExtended continuants

TheoremReflection formula for the order of extended continuants#●ready to prove

Let \(x : \mathbb{Z} \to \mathbb{Z}\) be an integer sequence and write \(K_a(x)_b\) for its extended continuant of order \(a\) with start index \(b\). For all integers \(h\) and \(n\),

\[K_{-n}(x)_h = (-1)^{n+1} K_{n-4}(x)_{h-n+2}.\]
public theorem_wanted extendedContinuant_neg_order (x : ℤ → ℤ) (h n : ℤ) :
    extendedContinuant x (-n) h =
      ((n + 1).negOnePow : ℤ) * extendedContinuant x (n - 4) (h - n + 2)
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Theorem 1.
Uses 1
Statement usesExtended continuants

TheoremBennett's continuant identity for nonnegative indices#●ready to prove

Let \(x : \mathbb{Z} \to \mathbb{Z}\) be an integer sequence and write \(K_a(x)_b\) for its extended continuant of order \(a\) with start index \(b\). For all nonnegative integers \(k\), \(\ell\), \(m\), \(n\),

\[(-1)^{k+\ell} K_{n-k-2}(x)_k K_{m-\ell-2}(x)_\ell + (-1)^{\ell+m} K_{n-\ell-2}(x)_\ell K_{k-m-2}(x)_m + (-1)^{m+k} K_{n-m-2}(x)_m K_{\ell-k-2}(x)_k = 0.\]
public theorem_wanted extendedContinuant_bennett_nat (x : ℤ → ℤ) (k ℓ m n : ℕ) :
    ((k + ℓ : ℤ).negOnePow : ℤ) * extendedContinuant x ((n : ℤ) - k - 2) k *
        extendedContinuant x ((m : ℤ) - ℓ - 2) ℓ +
      ((ℓ + m : ℤ).negOnePow : ℤ) * extendedContinuant x ((n : ℤ) - ℓ - 2) ℓ *
        extendedContinuant x ((k : ℤ) - m - 2) m +
      ((m + k : ℤ).negOnePow : ℤ) * extendedContinuant x ((n : ℤ) - m - 2) m *
        extendedContinuant x ((ℓ : ℤ) - k - 2) k = 0
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Theorem 2 (after G. T. Bennett, 1939).
Uses 1
Statement usesExtended continuants

TheoremBennett's continuant identity for all integer indices#●ready to prove

Let \(x : \mathbb{Z} \to \mathbb{Z}\) be an integer sequence and write \(K_a(x)_b\) for its extended continuant of order \(a\) with start index \(b\). For all integers \(k\), \(\ell\), \(m\), \(n\),

\[(-1)^{k+\ell} K_{n-k-2}(x)_k K_{m-\ell-2}(x)_\ell + (-1)^{\ell+m} K_{n-\ell-2}(x)_\ell K_{k-m-2}(x)_m + (-1)^{m+k} K_{n-m-2}(x)_m K_{\ell-k-2}(x)_k = 0.\]

This extends Bennett's identity from nonnegative to arbitrary integer indices.

public theorem_wanted extendedContinuant_bennett (x : ℤ → ℤ) (k ℓ m n : ℤ) :
    ((k + ℓ).negOnePow : ℤ) * extendedContinuant x (n - k - 2) k *
        extendedContinuant x (m - ℓ - 2) ℓ +
      ((ℓ + m).negOnePow : ℤ) * extendedContinuant x (n - ℓ - 2) ℓ *
        extendedContinuant x (k - m - 2) m +
      ((m + k).negOnePow : ℤ) * extendedContinuant x (n - m - 2) m *
        extendedContinuant x (ℓ - k - 2) k = 0
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Theorem 3.
Uses 1
Statement usesExtended continuants

TheoremEuler's continuant identity for extended continuants#●ready to prove

Let \(x : \mathbb{Z} \to \mathbb{Z}\) be an integer sequence and write \(K_a(x)_b\) for its extended continuant of order \(a\) with start index \(b\). For all integers \(h\), \(k\), \(\ell\), \(m\),

\[K_{\ell+m}(x)_h K_{k-1}(x)_{\ell+h+1} - K_{m-1}(x)_{\ell+h+1} K_{k+\ell}(x)_h = (-1)^k K_{m-k-2}(x)_{k+\ell+h+2} K_{\ell-1}(x)_h.\]
public theorem_wanted extendedContinuant_euler (x : ℤ → ℤ) (h k ℓ m : ℤ) :
    extendedContinuant x (ℓ + m) h * extendedContinuant x (k - 1) (ℓ + h + 1) -
        extendedContinuant x (m - 1) (ℓ + h + 1) * extendedContinuant x (k + ℓ) h =
      (k.negOnePow : ℤ) * extendedContinuant x (m - k - 2) (k + ℓ + h + 2) *
        extendedContinuant x (ℓ - 1) h
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Corollary 1.
Uses 1
Statement usesExtended continuants

TheoremDeterminant identity for extended continuants#●ready to prove

Let \(x : \mathbb{Z} \to \mathbb{Z}\) be an integer sequence and write \(K_a(x)_b\) for its extended continuant of order \(a\) with start index \(b\). For every integer \(n\),

\[K_n(x)_0 K_{n-2}(x)_1 - K_{n-1}(x)_1 K_{n-1}(x)_0 = (-1)^{n+1}.\]
public theorem_wanted extendedContinuant_det (x : ℤ → ℤ) (n : ℤ) :
    extendedContinuant x n 0 * extendedContinuant x (n - 2) 1 -
        extendedContinuant x (n - 1) 1 * extendedContinuant x (n - 1) 0 =
      ((n + 1).negOnePow : ℤ)
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Corollary 2.
Uses 1
Statement usesExtended continuants

TheoremNo silent sequences of even order#●ready to prove

Let \(\sigma \ge 0\) be an even integer and write \(K_a(x)_b\) for the extended continuant of order \(a\) with start index \(b\). For all bi-infinite integer sequences \(x, z : \mathbb{Z} \to \mathbb{Z}\) it is not the case that \(K_{-i-\sigma-1}(x)_0 = K_i(z)_0\) and \(K_{-i-\sigma-2}(x)_1 = K_{i-1}(z)_1\) for every natural number \(i\).

In the paper's terms: for even \(\sigma\) no bi-infinite sequence \(x\) is \(\sigma\)-silent, that is, there is no sequence \(z\) such that for every \(i \ge 0\) the raw westbound convergent \(k_{-i-\sigma-1} = K_{-i-\sigma-1}(x)_0 / K_{-i-\sigma-2}(x)_1\) of \(x\) is strictly equivalent (equal numerators and equal denominators) to the raw convergent \(d_i = K_i(z)_0 / K_{i-1}(z)_1\) of \(z\). The BpCF conditions are not needed.

public theorem_wanted not_silent_of_even (x z : ℤ → ℤ) (σ : ℕ) (hσ : Even σ) :
    ¬ ∀ i : ℕ, extendedContinuant x (-(i : ℤ) - σ - 1) 0 = extendedContinuant z i 0 ∧
      extendedContinuant x (-(i : ℤ) - σ - 2) 1 = extendedContinuant z ((i : ℤ) - 1) 1
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Theorem 4.
Uses 1
Statement usesExtended continuants

TheoremTerms of a \(1\)-silent sequence#●ready to prove

Let \(x, y, z : \mathbb{Z} \to \mathbb{Z}\) be bi-infinite integer sequences and write \(K_a(x)_b\) for the extended continuant of order \(a\) with start index \(b\). Suppose that for every natural number \(i\), \(K_i(x)_0 = K_i(y)_0\), \(K_{i-1}(x)_1 = K_{i-1}(y)_1\), \(K_{-i-2}(x)_0 = K_i(z)_0\) and \(K_{-i-3}(x)_1 = K_{i-1}(z)_1\). Then \(x_n = y_n\) for every \(n \ge 0\), \(x_{-n} = -z_n\) for every \(n \ge 1\), and \(z_0 = 0\).

In the paper's terms the hypotheses say that the raw convergents \(k_i = K_i(x)_0 / K_{i-1}(x)_1\) of \(x\) are strictly equivalent (equal numerators and equal denominators) to the raw convergents \(c_i\) of \(y\), and \(k_{-i-2}\) to the raw convergents \(d_i\) of \(z\), for all \(i \ge 0\). The conclusion \(z_0 = 0\) matches the paper's \(0 < \bar\alpha < 1\) for the EA-generated SCF of the irrational \(\bar\alpha\).

public theorem_wanted oneSilent_terms (x y z : ℤ → ℤ)
    (heast : ∀ i : ℕ, extendedContinuant x i 0 = extendedContinuant y i 0 ∧
      extendedContinuant x ((i : ℤ) - 1) 1 = extendedContinuant y ((i : ℤ) - 1) 1)
    (hwest : ∀ i : ℕ, extendedContinuant x (-(i : ℤ) - 2) 0 = extendedContinuant z i 0 ∧
      extendedContinuant x (-(i : ℤ) - 3) 1 = extendedContinuant z ((i : ℤ) - 1) 1) :
    (∀ n : ℕ, x n = y n) ∧ (∀ n : ℕ, 1 ≤ n → x (-(n : ℤ)) = -z n) ∧ z 0 = 0
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Theorem 5.
Uses 1
Statement usesExtended continuants

TheoremTerms of 3-silent sequences#●ready to prove

Let \(x, y, z : \mathbb{Z} \to \mathbb{Z}\) be bi-infinite integer sequences, and write \(K_a(x)_b\) for the extended continuant of \(x\) of order \(a\) with start index \(b\). Suppose that for every natural number \(i\) we have \(K_i(x)_0 = K_i(y)_0\), \(K_{i-1}(x)_1 = K_{i-1}(y)_1\), \(K_{-i-4}(x)_0 = K_i(z)_0\) and \(K_{-i-5}(x)_1 = K_{i-1}(z)_1\), and that \(x_{-1} = 0\). Then \(x_n = y_n\) for every \(n \ge 0\), and \(x_{-n} = -z_{n-2}\) for every \(n \ge 2\).

In the paper's terms, the hypotheses say that the raw convergents \(k_n = K_n(x)_0 / K_{n-1}(x)_1\) of \(x\) satisfy \(k_i \doteq c_i\) and \(k_{-i-4} \doteq d_i\) for all \(i \ge 0\), where \(c_i\) and \(d_i\) are the corresponding raw convergents of \(y\) and \(z\) and \(\doteq\) is equality of numerators and of denominators; the periodicity and limit conditions of a bi-infinite periodic continued fraction are not assumed.

public theorem_wanted threeSilent_terms (x y z : ℤ → ℤ)
    (heast : ∀ i : ℕ, extendedContinuant x i 0 = extendedContinuant y i 0 ∧
      extendedContinuant x ((i : ℤ) - 1) 1 = extendedContinuant y ((i : ℤ) - 1) 1)
    (hwest : ∀ i : ℕ, extendedContinuant x (-(i : ℤ) - 4) 0 = extendedContinuant z i 0 ∧
      extendedContinuant x (-(i : ℤ) - 5) 1 = extendedContinuant z ((i : ℤ) - 1) 1)
    (hx : x (-1) = 0) :
    (∀ n : ℕ, x n = y n) ∧ ∀ n : ℕ, 2 ≤ n → x (-(n : ℤ)) = -z ((n : ℤ) - 2)
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Theorem 6 and its proof (option 2, x_{-1} = 0).
Uses 1
Statement usesExtended continuants

TheoremTerms of a \(\sigma\)-silent sequence for odd \(\sigma \ge 5\)#●ready to prove

Let \(\sigma \ge 5\) be an odd integer, let \(x, y, z : \mathbb{Z} \to \mathbb{Z}\) be bi-infinite integer sequences, and write \(K_a(x)_b\) for the extended continuant of order \(a\) with start index \(b\). Suppose that for every natural number \(i\), \(K_i(x)_0 = K_i(y)_0\), \(K_{i-1}(x)_1 = K_{i-1}(y)_1\), \(K_{-i-\sigma-1}(x)_0 = K_i(z)_0\) and \(K_{-i-\sigma-2}(x)_1 = K_{i-1}(z)_1\). Then \(x_n = y_n\) for every \(n \ge 0\), \(x_{-\sigma+2} x_{-\sigma+1} = -1 + K_{\sigma-6}(x)_{-\sigma+4} + z_0 K_{\sigma-5}(x)_{-\sigma+4}\), \(x_{-\sigma+1} = -K_{\sigma-5}(x)_{-\sigma+3} - z_0 K_{\sigma-4}(x)_{-\sigma+3}\), \(x_{-\sigma} = -K_{\sigma-3}(x)_{-\sigma+2} - z_1\), and \(x_{-n} = -z_{n-\sigma+1}\) for every integer \(n \ge \sigma + 1\).

The paper states the second formula as a quotient for \(x_{-\sigma+2}\); here it is multiplied out.

public theorem_wanted oddSilent_terms (x y z : ℤ → ℤ) (σ : ℤ) (hσ : Odd σ) (h5 : 5 ≤ σ)
    (heast : ∀ i : ℕ, extendedContinuant x i 0 = extendedContinuant y i 0 ∧
      extendedContinuant x ((i : ℤ) - 1) 1 = extendedContinuant y ((i : ℤ) - 1) 1)
    (hwest : ∀ i : ℕ, extendedContinuant x (-(i : ℤ) - σ - 1) 0 = extendedContinuant z i 0 ∧
      extendedContinuant x (-(i : ℤ) - σ - 2) 1 = extendedContinuant z ((i : ℤ) - 1) 1) :
    (∀ n : ℕ, x n = y n) ∧
      x (-σ + 2) * x (-σ + 1) = -1 + extendedContinuant x (σ - 6) (-σ + 4) +
        z 0 * extendedContinuant x (σ - 5) (-σ + 4) ∧
      x (-σ + 1) = -extendedContinuant x (σ - 5) (-σ + 3) -
        z 0 * extendedContinuant x (σ - 4) (-σ + 3) ∧
      x (-σ) = -extendedContinuant x (σ - 3) (-σ + 2) - z 1 ∧
      ∀ n : ℤ, σ + 1 ≤ n → x (-n) = -z (n - σ + 1)
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Theorem 7.
Uses 1
Statement usesExtended continuants

TheoremSilent-term formulas on table (33), case \(\sigma \equiv 1 \pmod 6\)#●ready to prove

Let \(\sigma \ge 7\) be an integer with \(\sigma \equiv 1 \pmod 6\), let \(c_1 \ne c_2\) be integers, and let \(x : \mathbb{Z} \to \mathbb{Z}\) be a bi-infinite integer sequence with \(x_{-3} = x_0 + c_1\), \(x_{-2} = 1\), \(x_{-1} = -1\) and, for all integers \(4 \le m \le \sigma - 3\), \(x_{-m} = -1\) if \(m \equiv 1 \pmod 3\) and \(x_{-m} = 1\) otherwise. Write \(K_a(x)_b\) for the extended continuant of order \(a\) with start index \(b\), and put \(z_0 = x_0 + c_2\) and \(w = -K_{\sigma-5}(x)_{-\sigma+3} - z_0 K_{\sigma-4}(x)_{-\sigma+3}\). Then \(w \ne 0\) and \(-1 + K_{\sigma-6}(x)_{-\sigma+4} + z_0 K_{\sigma-5}(x)_{-\sigma+4} = w\).

So formula (29) of Theorem 7, with \(z_0 = x_0 + c_2\), gives \(x_{-\sigma+1} = w \ne 0\) and \(x_{-\sigma+2} = 1\).

public theorem_wanted silentTerms_table_one_mod_six (x : ℤ → ℤ) (σ : ℤ) (hσ : σ % 6 = 1)
    (h7 : 7 ≤ σ) (c₁ c₂ : ℤ) (hc : c₁ ≠ c₂) (h3 : x (-3) = x 0 + c₁) (h2 : x (-2) = 1)
    (h1 : x (-1) = -1)
    (htab : ∀ m : ℤ, 4 ≤ m → m ≤ σ - 3 → x (-m) = if m % 3 = 1 then -1 else 1) :
    -extendedContinuant x (σ - 5) (-σ + 3) - (x 0 + c₂) * extendedContinuant x (σ - 4) (-σ + 3)
        ≠ 0 ∧
      -1 + extendedContinuant x (σ - 6) (-σ + 4) +
          (x 0 + c₂) * extendedContinuant x (σ - 5) (-σ + 4) =
        1 * (-extendedContinuant x (σ - 5) (-σ + 3) -
          (x 0 + c₂) * extendedContinuant x (σ - 4) (-σ + 3))
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Proposition 3 (case σ ≡ 1 mod 6).
Uses 1
Statement usesExtended continuants

TheoremSilent-term formulas on table (33), case \(\sigma \equiv 5 \pmod 6\)#●ready to prove

Let \(\sigma \ge 7\) be an integer with \(\sigma \equiv 5 \pmod 6\), let \(c_1 \ne c_2\) be integers, and let \(x : \mathbb{Z} \to \mathbb{Z}\) be a bi-infinite integer sequence with \(x_{-3} = x_0 + c_1\), \(x_{-2} = 1\), \(x_{-1} = -1\) and, for all integers \(4 \le m \le \sigma - 3\), \(x_{-m} = -1\) if \(m \equiv 2 \pmod 3\) and \(x_{-m} = 1\) otherwise. Write \(K_a(x)_b\) for the extended continuant of order \(a\) with start index \(b\), and put \(z_0 = x_0 + c_2\) and \(w = -K_{\sigma-5}(x)_{-\sigma+3} - z_0 K_{\sigma-4}(x)_{-\sigma+3}\). Then \(w \ne 0\) and \(-1 + K_{\sigma-6}(x)_{-\sigma+4} + z_0 K_{\sigma-5}(x)_{-\sigma+4} = (1 + c_2 - c_1) w\).

So formula (29) of Theorem 7, with \(z_0 = x_0 + c_2\), gives \(x_{-\sigma+1} = w \ne 0\) and \(x_{-\sigma+2} = 1 + c_2 - c_1\).

public theorem_wanted silentTerms_table_five_mod_six (x : ℤ → ℤ) (σ : ℤ) (hσ : σ % 6 = 5)
    (h7 : 7 ≤ σ) (c₁ c₂ : ℤ) (hc : c₁ ≠ c₂) (h3 : x (-3) = x 0 + c₁) (h2 : x (-2) = 1)
    (h1 : x (-1) = -1)
    (htab : ∀ m : ℤ, 4 ≤ m → m ≤ σ - 3 → x (-m) = if m % 3 = 2 then -1 else 1) :
    -extendedContinuant x (σ - 5) (-σ + 3) - (x 0 + c₂) * extendedContinuant x (σ - 4) (-σ + 3)
        ≠ 0 ∧
      -1 + extendedContinuant x (σ - 6) (-σ + 4) +
          (x 0 + c₂) * extendedContinuant x (σ - 5) (-σ + 4) =
        (1 + c₂ - c₁) * (-extendedContinuant x (σ - 5) (-σ + 3) -
          (x 0 + c₂) * extendedContinuant x (σ - 4) (-σ + 3))
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Proposition 3 (case σ ≡ 5 mod 6).
Uses 1
Statement usesExtended continuants

TheoremThe conjugate continued fraction is not purely periodic#●ready to prove

Let \(P\), \(Q\) and \(D\) be integers with \(D > 0\) not a perfect square and \(Q > 0\), and let \(\bar\alpha = (P - \sqrt{D})/Q\). Then the simple continued fraction \([a_0; a_1, a_2, \dots]\) of \(\bar\alpha\), which is infinite because \(\bar\alpha\) is irrational, is not purely periodic: there is no integer \(s \ge 1\) with \(a_{n+s} = a_n\) for all \(n \ge 0\). Here \(a_0 = \lfloor \bar\alpha \rfloor\) is included.

public theorem_wanted conjugate_continuedFraction_not_purelyPeriodic (P Q D : ℤ) (hD : 0 < D)
    (hsq : ¬ IsSquare D) (hQ : 0 < Q) :
    ¬ ∃ s : ℕ, 0 < s ∧ ∀ n : ℕ,
      (GenContFract.IntFractPair.stream (((P : ℝ) - √(D : ℝ)) / Q) (n + s)).map (·.b) =
        (GenContFract.IntFractPair.stream (((P : ℝ) - √(D : ℝ)) / Q) n).map (·.b)
Sources
  • Dixon J. Jones, Extended Continuants and Bi-infinite Periodic Continued Fractions, INTEGERS 26 (2026), Article A73, Lemma 3.
8 fully proved13 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.