Zaremba Five Finite Front

Abstract

A fuelled Euclidean checker and a kernel-decided witness table certify the bound five for every denominator from two through 1024.

The quotient trace records the Euclidean quotient and recurses on the strictly smaller remainder. The Boolean checker separately tests coprimality, numerator range, and the digit bound.

Definition 1.1 (Fuelled Euclidean quotient trace).

$$\begin{array}{c}cfDigitsAux:\mathbb{N}\to \mathbb{N}\to \mathbb{N}\to \mathrm{List}\left(\mathbb{N}\right),\\ \forall a,q\in \mathbb{N},\mathrm{cfDigitsAux}\left(0,a,q\right)=[],\\ \forall fuel,a,q\in \mathbb{N},\mathrm{cfDigitsAux}\left(fuel+1,a,q\right)=\mathrm{if}\left(q=0,[],\mathrm{cons}\left(\lfloor \frac{a}{q}\rfloor ,\mathrm{cfDigitsAux}\left(fuel,q,a\mathrm{mod}q\right)\right)\right).\end{array}$$

Formalization. D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.cfDigitsAux (✓ std3).

Source. Repository-derived.

Commentary.

The zero-fuel trace is empty. At positive fuel, a zero divisor again gives the empty trace; otherwise the next digit is the natural-number quotient and recursion continues with the divisor and remainder.

Definition 1.2 (Continued-fraction digits).

$$\forall a,q\in \mathbb{N},\mathrm{cfDigits}\left(a,q\right)=\mathrm{cfDigitsAux}\left(q+1,a,q\right).$$

Formalization. D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.cfDigits (✓ std3).

Source. Repository-derived.

Commentary.

The public quotient trace starts the fuelled recursion with q plus one steps.

Definition 1.3 (Zaremba witness).

$$\forall A,a,q\in \mathbb{N},\mathrm{ZarembaWitness}\left(A,a,q\right)⟺(\mathrm{Coprime}\left(a,q\right)\wedge (0<a\wedge (a<q\wedge (\forall d\in \mathrm{cfDigits}\left(a,q\right),d\le A)))).$$

Formalization. D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.ZarembaWitness (✓ std3).

Source. Repository-derived.

Commentary.

A witness is coprime to the denominator, lies strictly between zero and the denominator, and has every continued-fraction digit at most A.

Definition 1.4 (Zaremba Boolean checker).

$$\forall A,a,q\in \mathbb{N},\mathrm{zarembaCheck}\left(A,a,q\right)=((\mathrm{decide}\left(\mathrm{Coprime}\left(a,q\right)\right))\wedge (\mathrm{decide}\left(0<a\right))\wedge (\mathrm{decide}\left(a<q\right))\wedge (\mathrm{digitsBounded}\left(A,\mathrm{cfDigits}\left(a,q\right)\right))).$$

Formalization. D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.zarembaCheck (✓ std3).

Source. Repository-derived.

Commentary.

The checker is the Boolean conjunction of the three arithmetic tests and the bounded-digits test.

Definition 1.5 (Explicit Zaremba-five witness table).

$$zarembaFiveWitnessTable:\mathrm{List}\left(\mathbb{N}\right).$$

Formalization. D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.zarembaFiveWitnessTable (✓ std3).

Source. Repository-derived.

Commentary.

This is the explicit kernel-decided list of numerator witnesses indexed by q from zero through 1024. Its concrete Lean value has length 1025.

Definition 1.6 (Zaremba-five numerator lookup).

$$\forall q\in \mathbb{N},\mathrm{zarembaFiveNumerator}\left(q\right)=\mathrm{getD}\left(zarembaFiveWitnessTable,q,0\right).$$

Formalization. D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.zarembaFiveNumerator (✓ std3).

Source. Repository-derived.

Commentary.

The numerator for q is the q-th table entry, with zero as the out-of-range default.

Theorem 1.7 (Euclidean checker soundness).

$$\begin{gathered} (\forall a,q\in \mathbb{N},0<q\Rightarrow \mathrm{cfDigits}\left(a,q\right)=\mathrm{cons}\left(\lfloor \frac{a}{q}\rfloor ,\mathrm{cfDigitsAux}\left(q,q,a\mathrm{mod}q\right)\right))\wedge \\ (\forall a,q\in \mathbb{N},0<q\Rightarrow a\mathrm{mod}q<q)\wedge \\ (\forall A,a,q\in \mathbb{N},\mathrm{zarembaCheck}\left(A,a,q\right)=true\Rightarrow \mathrm{ZarembaWitness}\left(A,a,q\right)). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

These three clauses expose the quotient-remainder recursion, strict remainder descent, and Boolean-to-propositional soundness.

Theorem 1.8 (Public finite Zaremba certificate).

$$\mathrm{all}\left(\mathrm{range}\left(1025\right),(q\mapsto \mathrm{decide}\left(q<2\right)\vee \mathrm{zarembaCheck}\left(5,\mathrm{zarembaFiveNumerator}\left(q\right),q\right))\right)=true.$$

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

Source. Repository-derived.

Commentary.

This publicly addressable theorem is the named finite escape witness. Lean’s kernel evaluates all 1025 rows of the witness table.

Theorem 1.9 (Zaremba five through 1024).

$$\begin{gathered} (\forall q\in \mathbb{N},2\le q\Rightarrow q\le 1024\Rightarrow \exists a\in \mathbb{N},\mathrm{ZarembaWitness}\left(5,a,q\right))\wedge \\ \mathrm{ZarembaWitness}\left(5,1,2\right)\wedge \\ (\mathrm{ZarembaWitness}\left(5,17,54\right)\wedge \forall a\in \mathrm{Fin}\left(17\right),\neg \mathrm{ZarembaWitness}\left(5,\mathrm{val}\left(a\right),54\right))\wedge \\ \mathrm{cfDigits}\left(17,54\right)=[0,3,5,1,2]\wedge \\ (\mathrm{cfDigits}\left(1,6\right)=[0,6]\wedge \mathrm{zarembaCheck}\left(5,1,6\right)=false). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The embedded 1025-row table is checked by Lean’s kernel decision procedure. Each admissible denominator selects its table row and checker soundness converts that row into a witness.

The remaining conjuncts pin the smallest denominator, the minimal numerator at 54, two exact quotient traces, and rejection when the digit six exceeds the bound five.

References

• Truth anchor: D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.ZarembaWitness
• Truth anchor: D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.cfDigits
• Truth anchor: D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.cfDigitsAux
• Truth anchor: D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.cfDigits_checker_sound
• Truth anchor: D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.zarembaCheck
• Truth anchor: D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.zarembaFiveCertificate
• Truth anchor: D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.zarembaFiveNumerator
• Truth anchor: D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.zarembaFiveWitnessTable
• Truth anchor: D5/S1/Depth/ContinuedFractions/ZarembaFiveFiniteFront.zaremba_five_upto_certified