Continued fractions of quadratic irrationals

DefinitionConvergent denominators as continuants#✓fully proved

For a sequence of natural numbers \(a_0, a_1, a_2, \dots\), its convergent denominators \(q_0, q_1, q_2, \dots\) are the natural numbers defined by \(q_0 = 1\), \(q_1 = a_1\) and \(q_{i+2} = a_{i+2} q_{i+1} + q_i\) for \(i \ge 0\). They are the denominators of the convergents of \([a_0; a_1, a_2, \dots]\), and \(q_i\) is the continuant \(K(a_1, \dots, a_i)\); the term \(a_0\) is never used.

The denominators \(r_i\) of the paper, those of the convergents of \([a_1; a_2, \dots, a_i]\), are the convergent denominators of the shifted sequence \((a_{n+1})_{n \ge 0}\) at index \(i - 1\), for \(i \ge 1\).

def convergentDen (a : ℕ → ℕ) : ℕ → ℕ
  | 0 => 1
  | 1 => a 1
  | n + 2 => a (n + 2) * convergentDen a (n + 1) + convergentDen a n
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, notation of Proposition 2.
Used by 14
Used byRecurrence for the convergent denominators · The convergent denominator \(q_1\) equals \(a_1\) · Parity of \(q_{l-1}\) for a symmetric sequence, even \(l\) · Parity of \(q_{l-1}\) for a symmetric sequence, odd \(l\) · Splitting the last convergent denominator of a symmetric sequence · The convergent denominator \(q_2\) equals \(a_2 a_1 + 1\) · The convergent denominator \(q_0\) equals \(1\) · Parity criterion for \((1 + \sqrt{d})/2\) with a given symmetric period · Parity of the shifted continuant of a symmetric sequence, even length · Parity of the shifted continuant of a symmetric sequence, odd length · Splitting the shifted continuant of a symmetric sequence · Parity criterion for \(\sqrt{d}\) with a given symmetric period, even length · Parity criterion for \(\sqrt{d}\) with a given symmetric period, odd length · Parity criterion for \(\sqrt{d}\) with a given symmetric period

TheoremThe convergent denominator \(q_0\) equals \(1\)#✓fully proved

For every sequence of natural numbers \(a_0, a_1, a_2, \dots\) with convergent denominators \(q_0, q_1, q_2, \dots\), we have \(q_0 = 1\).

theorem convergentDen_zero (a : ℕ → ℕ) : convergentDen a 0 = 1
Sources
  • Jun Ho Lee, INTEGERS 26 (2026), Article A69, notation of Proposition 2.
Uses 1
Statement usesConvergent denominators as continuants

TheoremThe convergent denominator \(q_1\) equals \(a_1\)#✓fully proved

For every sequence of natural numbers \(a_0, a_1, a_2, \dots\) with convergent denominators \(q_0, q_1, q_2, \dots\), we have \(q_1 = a_1\).

theorem convergentDen_one (a : ℕ → ℕ) : convergentDen a 1 = a 1
Sources
  • Jun Ho Lee, INTEGERS 26 (2026), Article A69, notation of Proposition 2.
Uses 1
Statement usesConvergent denominators as continuants

TheoremRecurrence for the convergent denominators#✓fully proved

For every sequence of natural numbers \(a_0, a_1, a_2, \dots\) with convergent denominators \(q_0, q_1, q_2, \dots\) and every natural number \(n\), we have \(q_{n+2} = a_{n+2} q_{n+1} + q_n\).

theorem convergentDen_add_two (a : ℕ → ℕ) (n : ℕ) :
    convergentDen a (n + 2) = a (n + 2) * convergentDen a (n + 1) + convergentDen a n
Sources
  • Jun Ho Lee, INTEGERS 26 (2026), Article A69, notation of Proposition 2.
Uses 1
Statement usesConvergent denominators as continuants

TheoremThe convergent denominator \(q_2\) equals \(a_2 a_1 + 1\)#✓fully proved

For every sequence of natural numbers \(a_0, a_1, a_2, \dots\) with convergent denominators \(q_0, q_1, q_2, \dots\), we have \(q_2 = a_2 a_1 + 1\).

theorem convergentDen_two (a : ℕ → ℕ) : convergentDen a 2 = a 2 * a 1 + 1
Sources
  • Jun Ho Lee, INTEGERS 26 (2026), Article A69, notation of Proposition 2.
Uses 1
Statement usesConvergent denominators as continuants

DefinitionContinued fractions with a prescribed period#✓fully proved

For a real number \(x\), natural numbers \(a_0\), \(l\), \(c\) and a sequence of natural numbers \(a_1, a_2, \dots\), we write \(x = [a_0; \overline{a_1, \dots, a_{l-1}, c}]\) when the regular continued fraction of \(x\) is the infinite expansion \([a_0; a_1, \dots, a_{l-1}, c, a_1, \dots, a_{l-1}, c, \dots]\): its integer part is \(a_0\), and for every \(k \ge 1\) its \(k\)-th partial quotient exists and equals \(c\) when \(l\) divides \(k\) and \(a_{k \bmod l}\) otherwise. The period \(l\) need not be minimal.

def HasPeriodicCF (x : ℝ) (a₀ : ℕ) (a : ℕ → ℕ) (l c : ℕ) : Prop :=
  (GenContFract.of x).h = a₀ ∧ ∀ n : ℕ, (GenContFract.of x).partDens.get? n =
    some (if (n + 1) % l = 0 then (c : ℝ) else (a ((n + 1) % l) : ℝ))
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, the expansions √d = [a₀; a₁, …, a_{l-1}, 2a₀] of Theorem 1.
Used by 10
Used byThe integer part of a periodic continued fraction is the floor · Parity criterion for \((1 + \sqrt{d})/2\) with a given symmetric period · Existence of \((1 + \sqrt{d})/2\) with a given symmetric period · Every parity pattern is realized by \((1 + \sqrt{d})/2\) for odd period length · Unrealizable parity patterns for \((1 + \sqrt d)/2\) with even \(l\) · Parity criterion for \(\sqrt{d}\) with a given symmetric period, even length · Parity criterion for \(\sqrt{d}\) with a given symmetric period, odd length · Parity criterion for \(\sqrt{d}\) with a given symmetric period · Number of unrealizable parity patterns for \(\sqrt{d}\), even length · Number of unrealizable parity patterns for \(\sqrt{d}\), odd length

TheoremThe integer part of a periodic continued fraction is the floor#✓fully proved

Let \(x\) be a real number and let \(a_0\), \(l\), \(c\) and \(a_1, a_2, \dots\) be natural numbers. Suppose that the regular continued fraction of \(x\) has integer part \(a_0\) and that, for every \(k \ge 1\), its \(k\)-th partial quotient is \(c\) when \(l\) divides \(k\) and \(a_r\) otherwise, where \(r\) is the remainder of \(k\) modulo \(l\) (so \(r = k\) when \(l = 0\)). For \(l \ge 1\) this says that the continued fraction is \([a_0; a_1, \dots, a_{l-1}, c, a_1, \dots, a_{l-1}, c, \dots]\). Then \(\lfloor x \rfloor = a_0\).

theorem HasPeriodicCF.floor_eq {x : ℝ} {a₀ : ℕ} {a : ℕ → ℕ} {l c : ℕ}
    (h : HasPeriodicCF x a₀ a l c) : ⌊x⌋ = a₀
Sources
  • Jun Ho Lee, INTEGERS 26 (2026), Article A69, Theorem 1 (a₀ = ⌊√d⌋).
Uses 1
Statement usesContinued fractions with a prescribed period

TheoremParity criterion for \(\sqrt{d}\) with a given symmetric period, odd length#●ready to prove

Let \(l\) be odd and let \(a_1, \dots, a_{l-1}\) be positive integers with \(a_i = a_{l-i}\) for \(1 \le i \le l - 1\). For \(0 \le i \le l - 1\) let \(q_i = K(a_1, \dots, a_i)\) be the continuant, given by \(q_0 = 1\), \(q_1 = a_1\) and \(q_{i+2} = a_{i+2} q_{i+1} + q_i\). Then there are a natural number \(d\) that is not a perfect square and a natural number \(a_0\) with \(\sqrt{d} = [a_0; \overline{a_1, \dots, a_{l-1}, 2a_0}]\) if and only if \(q_{l-1}\) is odd.

The paper fixes \(d\) in its preamble; here \(d\) and \(a_0\) are quantified existentially, as in its Proposition 2.

public theorem_wanted sqrt_hasPeriodicCF_exists_iff_of_odd (l : ℕ) (hl : Odd l) (a : ℕ → ℕ)
    (hpos : ∀ i, 1 ≤ i → i < l → 0 < a i)
    (hsymm : ∀ i, 1 ≤ i → i < l → a i = a (l - i)) :
    (∃ d a₀ : ℕ, ¬IsSquare d ∧ HasPeriodicCF √(d : ℝ) a₀ a l (2 * a₀)) ↔
      Odd (convergentDen a (l - 1))
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, Theorem 1 (i).
Uses 2
Statement usesContinued fractions with a prescribed period · Convergent denominators as continuants

TheoremParity criterion for \(\sqrt{d}\) with a given symmetric period, even length#●ready to prove

Let \(l \ge 2\) be even and let \(a_1, \dots, a_{l-1}\) be positive integers with \(a_i = a_{l-i}\) for \(1 \le i \le l - 1\). For \(0 \le i \le l - 1\) let \(q_i = K(a_1, \dots, a_i)\) be the continuant, given by \(q_0 = 1\), \(q_1 = a_1\) and \(q_{i+2} = a_{i+2} q_{i+1} + q_i\). Then there are a natural number \(d\) that is not a perfect square and a natural number \(a_0\) with \(\sqrt{d} = [a_0; \overline{a_1, \dots, a_{l-1}, 2a_0}]\) if and only if either \(a_{l/2}\) and \(q_{l-1}\) are both odd, or \(a_{l/2}\) is even.

public theorem_wanted sqrt_hasPeriodicCF_exists_iff_of_even (l : ℕ) (hl : Even l) (hl0 : 0 < l)
    (a : ℕ → ℕ) (hpos : ∀ i, 1 ≤ i → i < l → 0 < a i)
    (hsymm : ∀ i, 1 ≤ i → i < l → a i = a (l - i)) :
    (∃ d a₀ : ℕ, ¬IsSquare d ∧ HasPeriodicCF √(d : ℝ) a₀ a l (2 * a₀)) ↔
      (Odd (a (l / 2)) ∧ Odd (convergentDen a (l - 1))) ∨ Even (a (l / 2))
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, Theorem 1 (ii).
Uses 2
Statement usesContinued fractions with a prescribed period · Convergent denominators as continuants

TheoremSplitting the last convergent denominator of a symmetric sequence#●ready to prove

Let \(l\) be a natural number and let \(a_0, a_1, a_2, \dots\) be natural numbers with convergent denominators \(q_0, q_1, q_2, \dots\), such that \(a_i = a_{l-i}\) for \(1 \le i < l\). Then for every \(i\) with \(1 \le i \le l - 2\),

\[q_{l-1} = q_i q_{l-1-i} + q_{i-1} q_{l-2-i}.\]

The case \(i = 0\) of the paper, which uses \(q_{-1} = 0\), is omitted.

public theorem_wanted convergentDen_symm_split (l : ℕ) (a : ℕ → ℕ)
    (hsymm : ∀ i, 1 ≤ i → i < l → a i = a (l - i)) (i : ℕ) (hi : 1 ≤ i) (hil : i + 2 ≤ l) :
    convergentDen a (l - 1) =
      convergentDen a i * convergentDen a (l - 1 - i) +
        convergentDen a (i - 1) * convergentDen a (l - 2 - i)
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, Proposition 3 (i).
Uses 1
Statement usesConvergent denominators as continuants

TheoremSplitting the shifted continuant of a symmetric sequence#●ready to prove

Let \(l\) be a natural number and let \(a_1, \dots, a_{l-1}\) be natural numbers with \(a_i = a_{l-i}\) for \(1 \le i \le l - 1\). For \(j \ge 1\) let \(r_j = K(a_2, \dots, a_j)\) be the continuant, given by \(r_1 = 1\), \(r_2 = a_2\) and \(r_{j+2} = a_{j+2} r_{j+1} + r_j\). Then for every \(i\) with \(2 \le i \le l - 3\),

\[r_{l-2} = r_i \, r_{l-1-i} + r_{i-1} \, r_{l-2-i}.\]

The cases \(i \in \{0, 1, l - 2\}\) of the paper, which need \(r_0 = 0\) and \(r_{-1} = 1\), are omitted.

public theorem_wanted shifted_convergentDen_symm_split (l : ℕ) (a : ℕ → ℕ)
    (hsymm : ∀ i, 1 ≤ i → i < l → a i = a (l - i)) (i : ℕ) (hi : 2 ≤ i) (hil : i + 3 ≤ l) :
    convergentDen (fun n => a (n + 1)) (l - 3) =
      convergentDen (fun n => a (n + 1)) (i - 1) *
          convergentDen (fun n => a (n + 1)) (l - 2 - i) +
        convergentDen (fun n => a (n + 1)) (i - 2) *
          convergentDen (fun n => a (n + 1)) (l - 3 - i)
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, Proposition 3 (ii).
Uses 1
Statement usesConvergent denominators as continuants

TheoremParity of \(q_{l-1}\) for a symmetric sequence, even \(l\)#●ready to prove

Let \(l \ge 2\) be even and let \(a_0, a_1, a_2, \dots\) be natural numbers with convergent denominators \(q_0, q_1, q_2, \dots\), such that \(a_i = a_{l-i}\) for \(1 \le i < l\). Then \(q_{l-1} \equiv a_{l/2} \, q_{l/2-1} \pmod 2\).

public theorem_wanted convergentDen_parity_of_even (l : ℕ) (hl : Even l) (hl0 : 0 < l)
    (a : ℕ → ℕ) (hsymm : ∀ i, 1 ≤ i → i < l → a i = a (l - i)) :
    convergentDen a (l - 1) ≡ a (l / 2) * convergentDen a (l / 2 - 1) [MOD 2]
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, Corollary 1 (i).
Uses 1
Statement usesConvergent denominators as continuants

TheoremParity of the shifted continuant of a symmetric sequence, even length#●ready to prove

Let \(l \ge 4\) be even and let \(a_1, \dots, a_{l-1}\) be natural numbers with \(a_i = a_{l-i}\) for \(1 \le i \le l - 1\). For \(j \ge 1\) let \(r_j = K(a_2, \dots, a_j)\) be the continuant, given by \(r_1 = 1\), \(r_2 = a_2\) and \(r_{j+2} = a_{j+2} r_{j+1} + r_j\). Then \(r_{l-2} \equiv a_{l/2} \, r_{l/2-1} \pmod 2\).

The case \(l = 2\) of the paper, which needs \(r_0 = 0\), is omitted.

public theorem_wanted shifted_convergentDen_parity_of_even (l : ℕ) (hl : Even l) (hl4 : 4 ≤ l)
    (a : ℕ → ℕ) (hsymm : ∀ i, 1 ≤ i → i < l → a i = a (l - i)) :
    convergentDen (fun n => a (n + 1)) (l - 3) ≡
      a (l / 2) * convergentDen (fun n => a (n + 1)) (l / 2 - 2) [MOD 2]
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, Corollary 1 (ii).
Uses 1
Statement usesConvergent denominators as continuants

TheoremParity of \(q_{l-1}\) for a symmetric sequence, odd \(l\)#●ready to prove

Let \(l \ge 3\) be odd and let \(a_0, a_1, a_2, \dots\) be natural numbers with convergent denominators \(q_0, q_1, q_2, \dots\), such that \(a_i = a_{l-i}\) for \(1 \le i < l\). Then \(q_{l-1} \equiv q_{(l-1)/2} + q_{(l-3)/2} \pmod 2\).

public theorem_wanted convergentDen_parity_of_odd (l : ℕ) (hl : Odd l) (hl3 : 3 ≤ l)
    (a : ℕ → ℕ) (hsymm : ∀ i, 1 ≤ i → i < l → a i = a (l - i)) :
    convergentDen a (l - 1) ≡
      convergentDen a ((l - 1) / 2) + convergentDen a ((l - 3) / 2) [MOD 2]
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, Corollary 2 (i).
Uses 1
Statement usesConvergent denominators as continuants

TheoremParity of the shifted continuant of a symmetric sequence, odd length#●ready to prove

Let \(l \ge 5\) be odd and let \(a_1, \dots, a_{l-1}\) be natural numbers with \(a_i = a_{l-i}\) for \(1 \le i \le l - 1\). For \(j \ge 1\) let \(r_j = K(a_2, \dots, a_j)\) be the continuant, given by \(r_1 = 1\), \(r_2 = a_2\) and \(r_{j+2} = a_{j+2} r_{j+1} + r_j\). Then \(r_{l-2} \equiv r_{(l-1)/2} + r_{(l-3)/2} \pmod 2\).

The case \(l = 3\) of the paper, which needs \(r_0 = 0\), is omitted.

public theorem_wanted shifted_convergentDen_parity_of_odd (l : ℕ) (hl : Odd l) (hl5 : 5 ≤ l)
    (a : ℕ → ℕ) (hsymm : ∀ i, 1 ≤ i → i < l → a i = a (l - i)) :
    convergentDen (fun n => a (n + 1)) (l - 3) ≡
      convergentDen (fun n => a (n + 1)) ((l - 1) / 2 - 1) +
        convergentDen (fun n => a (n + 1)) ((l - 3) / 2 - 1) [MOD 2]
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, Corollary 2 (ii).
Uses 1
Statement usesConvergent denominators as continuants

TheoremNumber of unrealizable parity patterns for \(\sqrt{d}\), odd length#●ready to prove

Let \(l \ge 3\) be odd. Call a parity pattern \((v_1, \dots, v_{(l-1)/2}) \in (\mathbb{Z}/2)^{(l-1)/2}\) realizable if there are positive integers \(a_1, \dots, a_{l-1}\) with \(a_i = a_{l-i}\) for \(1 \le i \le l - 1\) and \(a_j \equiv v_j \pmod 2\) for \(1 \le j \le (l-1)/2\), a natural number \(d\) that is not a perfect square and a natural number \(a_0\) with \(\sqrt{d} = [a_0; \overline{a_1, \dots, a_{l-1}, 2a_0}]\). If \(A\) is the number of parity patterns that are not realizable, then \(3A = 2^{(l-1)/2} - (-1)^{(l-1)/2}\).

Writing \(A_m\) for \(A\) when \(l = 2m + 1\), this gives \(A_1 = A_2 = 1\) and \(A_m = A_{m-1} + 2A_{m-2}\) for \(m \ge 3\).

public theorem_wanted sqrt_periodicCF_obstruction_count_of_odd (l : ℕ) (hl : Odd l)
    (hl3 : 3 ≤ l) :
    3 * (Set.ncard {v : Fin (l / 2) → ZMod 2 | ¬∃ a : ℕ → ℕ,
        (∀ i, 1 ≤ i → i < l → 0 < a i) ∧ (∀ i, 1 ≤ i → i < l → a i = a (l - i)) ∧
        (∀ j : Fin (l / 2), (a ((j : ℕ) + 1) : ZMod 2) = v j) ∧
        ∃ d a₀ : ℕ, ¬IsSquare d ∧ HasPeriodicCF √(d : ℝ) a₀ a l (2 * a₀)} : ℤ) =
      2 ^ (l / 2) - (-1) ^ (l / 2)
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, Theorem 3.
Uses 1
Statement usesContinued fractions with a prescribed period

TheoremNumber of unrealizable parity patterns for \(\sqrt{d}\), even length#●ready to prove

Let \(l \ge 4\) be even. Call a parity pattern \((v_1, \dots, v_{l/2}) \in (\mathbb{Z}/2)^{l/2}\) realizable if there are positive integers \(a_1, \dots, a_{l-1}\) with \(a_i = a_{l-i}\) for \(1 \le i \le l - 1\) and \(a_j \equiv v_j \pmod 2\) for \(1 \le j \le l/2\), a natural number \(d\) that is not a perfect square and a natural number \(a_0\) with \(\sqrt{d} = [a_0; \overline{a_1, \dots, a_{l-1}, 2a_0}]\). If \(B\) is the number of parity patterns that are not realizable, then \(3B = 2^{l/2 - 1} - (-1)^{l/2 - 1}\).

public theorem_wanted sqrt_periodicCF_obstruction_count_of_even (l : ℕ) (hl : Even l)
    (hl4 : 4 ≤ l) :
    3 * (Set.ncard {v : Fin (l / 2) → ZMod 2 | ¬∃ a : ℕ → ℕ,
        (∀ i, 1 ≤ i → i < l → 0 < a i) ∧ (∀ i, 1 ≤ i → i < l → a i = a (l - i)) ∧
        (∀ j : Fin (l / 2), (a ((j : ℕ) + 1) : ZMod 2) = v j) ∧
        ∃ d a₀ : ℕ, ¬IsSquare d ∧ HasPeriodicCF √(d : ℝ) a₀ a l (2 * a₀)} : ℤ) =
      2 ^ (l / 2 - 1) - (-1) ^ (l / 2 - 1)
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, Theorem 4.
Uses 1
Statement usesContinued fractions with a prescribed period

TheoremEvery parity pattern is realized by \((1 + \sqrt{d})/2\) for odd period length#●ready to prove

Let \(l\) be odd. For every parity pattern \((v_1, \dots, v_{(l-1)/2}) \in (\mathbb{Z}/2)^{(l-1)/2}\) there are positive integers \(a_1, \dots, a_{l-1}\) with \(a_i = a_{l-i}\) for \(1 \le i \le l - 1\) and \(a_j \equiv v_j \pmod 2\) for \(1 \le j \le (l-1)/2\), a natural number \(d\) that is not a perfect square and a natural number \(a_0\) with \((1 + \sqrt{d})/2 = [a_0; \overline{a_1, \dots, a_{l-1}, 2a_0 - 1}]\). That is, the number \(A'_l\) of patterns that are not realized is \(0\).

public theorem_wanted half_one_add_sqrt_periodicCF_obstruction_count_of_odd (l : ℕ)
    (hl : Odd l) :
    Set.ncard {v : Fin (l / 2) → ZMod 2 | ¬∃ a : ℕ → ℕ,
        (∀ i, 1 ≤ i → i < l → 0 < a i) ∧ (∀ i, 1 ≤ i → i < l → a i = a (l - i)) ∧
        (∀ j : Fin (l / 2), (a ((j : ℕ) + 1) : ZMod 2) = v j) ∧
        ∃ d a₀ : ℕ, ¬IsSquare d ∧
          HasPeriodicCF ((1 + √(d : ℝ)) / 2) a₀ a l (2 * a₀ - 1)} = 0
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, Theorem 5.
Uses 1
Statement usesContinued fractions with a prescribed period

TheoremUnrealizable parity patterns for \((1 + \sqrt d)/2\) with even \(l\)#●ready to prove

Let \(l \ge 2\) be even. Call a parity pattern \((v_1, \dots, v_{l/2}) \in (\mathbb{Z}/2)^{l/2}\) realizable if there are positive integers \(a_1, \dots, a_{l-1}\) with \(a_i = a_{l-i}\) for \(1 \le i < l\) and \(a_j \equiv v_j \pmod 2\) for \(1 \le j \le l/2\), together with natural numbers \(d\) and \(a_0\) such that \(d \equiv 1 \pmod 4\), \(d\) is not a perfect square and the regular continued fraction of \((1 + \sqrt d)/2\) is

\[[a_0; a_1, \dots, a_{l-1}, 2a_0 - 1, a_1, \dots, a_{l-1}, 2a_0 - 1, \dots].\]

Then the number \(B'_l\) of parity patterns that are not realizable is \(2^{l/2 - 1}\).

Without the hypothesis \(d \equiv 1 \pmod 4\) one would get \(B'_2 = 0\), since \(d = 15\) realizes \(a_1 = 2\).

public theorem_wanted half_one_add_sqrt_periodicCF_obstruction_count_of_even (l : ℕ)
    (hl : Even l) (hl0 : 0 < l) :
    Set.ncard {v : Fin (l / 2) → ZMod 2 | ¬∃ a : ℕ → ℕ,
        (∀ i, 1 ≤ i → i < l → 0 < a i) ∧ (∀ i, 1 ≤ i → i < l → a i = a (l - i)) ∧
        (∀ j : Fin (l / 2), (a ((j : ℕ) + 1) : ZMod 2) = v j) ∧
        ∃ d a₀ : ℕ, d % 4 = 1 ∧ ¬IsSquare d ∧
          HasPeriodicCF ((1 + √(d : ℝ)) / 2) a₀ a l (2 * a₀ - 1)} = 2 ^ (l / 2 - 1)
Sources
  • Jun Ho Lee, Nonexistence of the Continued Fraction of a Quadratic Irrational Number with a Given Sequence, INTEGERS 26 (2026), Article A69, Theorem 6.
Uses 1
Statement usesContinued fractions with a prescribed period

TheoremParity criterion for \(\sqrt{d}\) with a given symmetric period#●ready to prove

Let \(l \ge 3\) and let \(a_1, \dots, a_{l-1}\) be positive integers with \(a_i = a_{l-i}\) for \(1 \le i < l\). Let \(q_j\) be the denominator of the \(j\)-th convergent of \([a_0; a_1, a_2, \dots]\) (so \(q_0 = 1\), \(q_1 = a_1\) and \(q_{j+2} = a_{j+2} q_{j+1} + q_j\)), and let \(r_{l-2}\) be the denominator of the \((l-3)\)-th convergent of \([a_1; a_2, a_3, \dots]\). There are natural numbers \(d\) and \(a_0\) with \(d\) not a perfect square and \(\sqrt{d} = [a_0; \overline{a_1, \dots, a_{l-1}, 2a_0}]\) if and only if \(q_{l-1}\) is odd, or \(q_{l-1}\) and \(r_{l-2}\) are even and \(q_{l-2}\) is odd.

public theorem_wanted sqrt_hasPeriodicCF_exists_iff_parity (l : ℕ) (hl : 3 ≤ l) (a : ℕ → ℕ)
    (hpos : ∀ i, 1 ≤ i → i < l → 0 < a i)
    (hsymm : ∀ i, 1 ≤ i → i < l → a i = a (l - i)) :
    (∃ d a₀ : ℕ, ¬IsSquare d ∧ HasPeriodicCF √(d : ℝ) a₀ a l (2 * a₀)) ↔
      Odd (convergentDen a (l - 1)) ∨
        (Even (convergentDen a (l - 1)) ∧ Even (convergentDen (fun n => a (n + 1)) (l - 3)) ∧
          Odd (convergentDen a (l - 2)))
Sources
  • Jun Ho Lee, Classification for Existence of the Continued Fraction Expansions of √D and (1 + √D)/2, INTEGERS 24 (2024), Article A50, Proposition 1.
Uses 2
Statement usesContinued fractions with a prescribed period · Convergent denominators as continuants

TheoremParity criterion for \((1 + \sqrt{d})/2\) with a given symmetric period#●ready to prove

Let \(l \ge 3\) and let \(a_1, \dots, a_{l-1}\) be positive integers with \(a_i = a_{l-i}\) for \(1 \le i < l\). Let \(q_j\) be the denominator of the \(j\)-th convergent of \([a_0; a_1, a_2, \dots]\) (so \(q_0 = 1\), \(q_1 = a_1\) and \(q_{j+2} = a_{j+2} q_{j+1} + q_j\)), and let \(r_{l-2}\) be the denominator of the \((l-3)\)-th convergent of \([a_1; a_2, a_3, \dots]\). There are natural numbers \(d\) and \(a_0\) with \(d \equiv 1 \pmod 4\), \(d\) not a perfect square, and \((1 + \sqrt{d})/2 = [a_0; \overline{a_1, \dots, a_{l-1}, 2a_0 - 1}]\) if and only if \(q_{l-1}\) is odd, or \(q_{l-2}\) and \(r_{l-2}\) are odd and \(q_{l-1}\) is even.

The restriction \(d \equiv 1 \pmod 4\) is needed: \((1 + \sqrt{2})/2 = [1; \overline{4, 1}]\) fits \(l = 6\) with \((a_1, \dots, a_5) = (4, 1, 4, 1, 4)\), where \(q_5 = 140\), \(q_4 = 29\) and \(r_4 = 6\) violate the criterion.

public theorem_wanted half_one_add_sqrt_hasPeriodicCF_exists_iff_parity (l : ℕ) (hl : 3 ≤ l)
    (a : ℕ → ℕ) (hpos : ∀ i, 1 ≤ i → i < l → 0 < a i)
    (hsymm : ∀ i, 1 ≤ i → i < l → a i = a (l - i)) :
    (∃ d a₀ : ℕ, d % 4 = 1 ∧ ¬IsSquare d ∧ HasPeriodicCF ((1 + √(d : ℝ)) / 2) a₀ a l (2 * a₀ - 1)) ↔
      Odd (convergentDen a (l - 1)) ∨
        (Odd (convergentDen a (l - 2)) ∧ Odd (convergentDen (fun n => a (n + 1)) (l - 3)) ∧
          Even (convergentDen a (l - 1)))
Sources
  • Jun Ho Lee, Classification for Existence of the Continued Fraction Expansions of √D and (1 + √D)/2, INTEGERS 24 (2024), Article A50, Proposition 2.
Uses 2
Statement usesContinued fractions with a prescribed period · Convergent denominators as continuants

TheoremExistence of \((1 + \sqrt{d})/2\) with a given symmetric period#●ready to prove

Let \(l\) be a natural number and \(a_1, \dots, a_{l-1}\) positive integers with \(a_i = a_{l-i}\) for \(1 \le i < l\). If \(l\) is odd, there are natural numbers \(d\) and \(a_0\) with \(d \equiv 1 \pmod 4\), \(d\) not a perfect square, and \((1 + \sqrt{d})/2 = [a_0; \overline{a_1, \dots, a_{l-1}, 2a_0 - 1}]\). If \(l\) is even and positive, such \(d\) and \(a_0\) exist if and only if \(a_{l/2}\) is odd.

public theorem_wanted half_one_add_sqrt_hasPeriodicCF_exists_classification (l : ℕ)
    (a : ℕ → ℕ) (hpos : ∀ i, 1 ≤ i → i < l → 0 < a i)
    (hsymm : ∀ i, 1 ≤ i → i < l → a i = a (l - i)) :
    (Odd l →
      ∃ d a₀ : ℕ, d % 4 = 1 ∧ ¬IsSquare d ∧ HasPeriodicCF ((1 + √(d : ℝ)) / 2) a₀ a l (2 * a₀ - 1)) ∧
    (Even l → 0 < l →
      ((∃ d a₀ : ℕ, d % 4 = 1 ∧ ¬IsSquare d ∧ HasPeriodicCF ((1 + √(d : ℝ)) / 2) a₀ a l (2 * a₀ - 1)) ↔
        Odd (a (l / 2))))
Sources
  • Jun Ho Lee, Classification for Existence of the Continued Fraction Expansions of √D and (1 + √D)/2, INTEGERS 24 (2024), Article A50, Theorem 3.
Uses 1
Statement usesContinued fractions with a prescribed period

TheoremFundamental unit from the period of \(\sqrt{d}\)#●ready to prove

Let \(d \ge 2\) be a squarefree integer, let \(\varepsilon\) be the least real number \(u > 1\) of the form \(u = (x + y\sqrt{d})/2\) with \(x, y \in \mathbb{Z}\) and \(x^2 - d y^2 = \pm 4\) (the fundamental unit of \(\mathbb{Q}(\sqrt{d})\)), let \(\sqrt{d} = [a_0; a_1, a_2, \dots]\) be the regular continued fraction of \(\sqrt{d}\), with convergents \(p_k / q_k\) (so \(p_0 = a_0\) and \(q_0 = 1\)), and let \(l\) be the least positive integer such that \(a_{k+l} = a_k\) for all \(k \ge 1\). Then \(p_{l-1} + q_{l-1}\sqrt{d} = \varepsilon\), or \(p_{l-1} + q_{l-1}\sqrt{d} = \varepsilon^3\) and \(d \equiv 5 \pmod 8\).

For squarefree \(d\) the numbers \((x + y\sqrt{d})/2\) above are exactly the units of the ring of integers of \(\mathbb{Q}(\sqrt{d})\). The paper's positive squarefree \(d\) is restricted to \(d \ge 2\), since \(\mathbb{Q}(\sqrt{1})\) is not a quadratic field.

public theorem_wanted fundamentalUnit_eq_convergent_or_cube (d : ℕ) (hd : Squarefree d)
    (hd2 : 2 ≤ d) (ε : ℝ)
    (hε : IsLeast {u : ℝ | 1 < u ∧ ∃ x y : ℤ,
      (x ^ 2 - d * y ^ 2 = 4 ∨ x ^ 2 - d * y ^ 2 = -4) ∧ u = (x + y * √(d : ℝ)) / 2} ε)
    (l : ℕ) (hl : IsLeast {l : ℕ | 0 < l ∧ ∀ k : ℕ,
      (GenContFract.of √(d : ℝ)).partDens.get? (k + l) =
        (GenContFract.of √(d : ℝ)).partDens.get? k} l) :
    (GenContFract.of √(d : ℝ)).nums (l - 1) + (GenContFract.of √(d : ℝ)).dens (l - 1) * √(d : ℝ) =
        ε ∨
      ((GenContFract.of √(d : ℝ)).nums (l - 1) +
          (GenContFract.of √(d : ℝ)).dens (l - 1) * √(d : ℝ) = ε ^ 3 ∧ d % 8 = 5)
Sources
  • Jun Ho Lee, Classification for Existence of the Continued Fraction Expansions of √D and (1 + √D)/2, INTEGERS 24 (2024), Article A50, Theorem 1.
7 fully proved16 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.