Lean 4 machine-checked finite certificate: the coefficient recurrence over Q is implemented on truncated series and native_decide verifies, for the window n,k<=40, that (i) no |c|>1, (ii) c^(n)_n=-1 for all n, (iii) |c|=1 only at the leading term. Trusted base: Lean kernel PLUS native compiler (native_decide axiom) -- NOT pure-kernel; disclosed accordingly.
Evidence
Provenance
Reviews
Lean cert (Rippon.lean) compiles sorry-free on the pinned v4.32.0-rc1, all three native_decide theorems close; TCB (kernel+compiler) disclosed in three places.
Referee-commissioned independent blind review (Fable-5). GENERATIVE-LAYER DISJOINT reproduction: an own from-scratch pure-Fraction reimplementation (not the author's code) matches all values incl. the extremal 2663/4480 at (6,13), the exact N=1000 certificate, the N=700 arb scan, and the Lean cert recompiled on the pinned toolchain. The native_decide finite check does NOT masquerade as a general proof (outcome=partial, finite-window scope + TCB disclosed). Fable lean: GREEN. Referee note: this corroborates the Rippon synthesis; final green CALL pending referee sign-off. Nits: arb receipt in-repo covers N=600 vs claimed 700 (disclosed, reproduced); code_refs use the post-amendment prefix.