Periodic Continued Fractions Are Quadratic

Abstract

Eventually periodic continued fractions yield nondegenerate quadratic equations through integer Mobius transfers.

Lemma 1.1 (Cross-multiplied transfers compose).

$$\forall M,N\in \mathrm{MobiusInt},x,y,z\in \mathbb{R},(\mathrm{Rel}\left(M,x,z\right)\wedge \mathrm{Rel}\left(N,z,y\right))\Rightarrow \mathrm{Rel}\left(\mathrm{comp}\left(M,N\right),x,y\right)$$

Proof. Machine-checked in Lean as D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.rel_comp (✓ std3). ∎

Source. Repository-derived.

Commentary.

If one integer linear-fractional transfer relates x to an intermediate value z and a second relates z to y, their matrix product relates x directly to y. The relation is cross-multiplied, so composition uses no division and assumes no denominator is nonzero.

Lemma 1.2 (A segment relates its endpoint complete quotients).

$$\forall x\in \mathbb{R},h:\mathrm{EventuallyPeriodicCF}\left(x\right),first,length\in \mathbb{N},\mathrm{Rel}\left(\mathrm{segment}\left(\mathrm{coefficient}\left(h\right),first,length\right),\mathrm{completeQuotient}\left(h,first\right),\mathrm{completeQuotient}\left(h,first+length\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.segment_rel (✓ std3). ∎

Source. Repository-derived.

Commentary.

The product of any consecutive block of inverse continued-fraction steps relates the complete quotient at the start of the block to the complete quotient at its end. This packages repeated inverse-step recurrence into one integer transfer matrix.

Lemma 1.3 (The transfer determinant is multiplicative).

$$\forall M,N\in \mathrm{MobiusInt},\det \left(\mathrm{comp}\left(M,N\right)\right)=\det \left(M\right)\cdot \det \left(N\right)$$

Proof. Machine-checked in Lean as D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.det_comp (✓ std3). ∎

Source. Repository-derived.

Commentary.

The determinant of the product transfer is the product of the two integer determinants. This is the usual two-by-two determinant identity written for the four-entry transfer representation.

Lemma 1.4 (A segment has alternating determinant).

$$\forall coefficient:\mathbb{N}\to \mathbb{Z},first,length\in \mathbb{N},\det \left(\mathrm{segment}\left(coefficient,first,length\right)\right)=(-1{)}^{length}$$

Proof. Machine-checked in Lean as D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.segment_det (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each inverse continued-fraction step has determinant minus one. Therefore a segment of the given length has determinant minus one to that length, and in particular every segment transfer is nondegenerate.

Lemma 1.5 (Nonnegative coefficients give nonnegative segment entries).

$$\forall coefficient:\mathbb{N}\to \mathbb{Z},first,length\in \mathbb{N},[\forall k\in \mathbb{N},k<length\Rightarrow 0\le \mathrm{coefficient}\left(first+k\right)]\Rightarrow 0\le a\left(\mathrm{segment}\left(coefficient,first,length\right)\right)\wedge 0\le b\left(\mathrm{segment}\left(coefficient,first,length\right)\right)\wedge 0\le c\left(\mathrm{segment}\left(coefficient,first,length\right)\right)\wedge 0\le d\left(\mathrm{segment}\left(coefficient,first,length\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.segment_entries_nonneg (✓ std3). ∎

Source. Repository-derived.

Commentary.

When every coefficient in a finite block is nonnegative, all four entries of its transfer matrix are nonnegative. The property is preserved as each inverse-step matrix is multiplied onto the remaining segment.

Lemma 1.6 (Positive coefficients make the upper-right entry positive).

$$\forall coefficient:\mathbb{N}\to \mathbb{Z},first,length\in \mathbb{N},(0<length\wedge [\forall k\in \mathbb{N},k<length\Rightarrow 0<\mathrm{coefficient}\left(first+k\right)])\Rightarrow 0<b\left(\mathrm{segment}\left(coefficient,first,length\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.segment_b_pos (✓ std3). ∎

Source. Repository-derived.

Commentary.

A nonempty segment whose coefficients are all positive has a strictly positive upper-right matrix entry. Positivity propagates from the first step, while nonnegativity of the other tail entries prevents cancellation.

Lemma 1.7 (A periodic block has positive upper-right entry).

$$\forall x\in \mathbb{R},h:\mathrm{EventuallyPeriodicCF}\left(x\right),0<b\left(\mathrm{segment}\left(\mathrm{coefficient}\left(h\right),\mathrm{start}\left(h\right),\mathrm{period}\left(h\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.period_segment_b_pos (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certified period has positive length, and every coefficient from the period start onward is positive. Applying the finite-segment positivity result makes the upper-right entry of the period transfer strictly positive.

Lemma 1.8 (The computed infinite continued fraction is irrational).

$$\forall x\in \mathbb{R},h:\mathrm{EventuallyPeriodicCF}\left(x\right),\mathrm{Irrational}\left(x\right)$$

Proof. Machine-checked in Lean as D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.computed_cf_irrational (✓ std3). ∎

Source. Repository-derived.

Commentary.

A certified coefficient is present at every position of the computed continued fraction. A rational real would instead have a terminating regular continued fraction, so the two properties are incompatible and the represented value must be irrational.

Lemma 1.9 (Quadratic equations transfer across nondegenerate segments).

$$\forall x,y\in \mathbb{R},M\in \mathrm{MobiusInt},u,v,w\in \mathbb{Z},(\det \left(M\right)\ne 0\wedge \mathrm{Rel}\left(M,x,y\right)\wedge (u\ne 0\vee v\ne 0\vee w\ne 0)\wedge u\cdot y^2+v\cdot y+w=0)\Rightarrow \exists a,b,c\in \mathbb{Z},(a\ne 0\vee b\ne 0\vee c\ne 0)\wedge a\cdot x^2+b\cdot x+c=0$$

Proof. Machine-checked in Lean as D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.quadratic_transfers_across_segment (✓ std3). ∎

Source. Repository-derived.

Commentary.

Suppose a nondegenerate integer transfer relates x to y and y satisfies a nonzero integer quadratic equation. Clearing the linear-fractional relation produces an integer quadratic equation for x. The nonzero determinant ensures that its three transformed coefficients cannot all vanish.

Theorem 1.10 (Eventual periodicity forces quadratic irrationality).

$$\forall x\in \mathbb{R},\mathrm{EventuallyPeriodicCF}\left(x\right)\Rightarrow (\mathrm{Irrational}\left(x\right)\wedge \exists a,b,c\in \mathbb{Z},(a\ne 0\vee b\ne 0\vee c\ne 0)\wedge a\cdot x^2+b\cdot x+c=0)$$

Proof. Machine-checked in Lean as D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.eventually_periodic_cf_implies_quadratic_irrational (✓ std3). ∎

Source. Repository-derived.

Commentary.

Repeating the complete quotient makes the period transfer fix the periodic tail. Cross-multiplication gives that tail a nonzero integer quadratic equation, with nonvanishing certified by the positive upper-right entry.

The prefix transfer has determinant plus or minus one, so the quadratic equation pulls back from the periodic tail to the original value. The infinite computed coefficient stream separately proves irrationality, giving Lagrange direction A.

References

• Truth anchor: D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.computed_cf_irrational
• Truth anchor: D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.det_comp
• Truth anchor: D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.eventually_periodic_cf_implies_quadratic_irrational
• Truth anchor: D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.period_segment_b_pos
• Truth anchor: D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.quadratic_transfers_across_segment
• Truth anchor: D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.rel_comp
• Truth anchor: D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.segment_b_pos
• Truth anchor: D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.segment_det
• Truth anchor: D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.segment_entries_nonneg
• Truth anchor: D5/S1/Depth/ContinuedFractions/PeriodicImpliesQuadratic.segment_rel
• Dependency: D5/S1/Depth/GoldenContinuedFraction