Lean 4 machine-checked finite certificates (native_decide; trusted base = Lean kernel + native compiler, NOT pure-kernel — disclosed): (F) the exact factorization f_n = -t^n ∏_{k<n} h(t f_k) coefficientwise for 1 ≤ n ≤ 30, degrees ≤ 60; (B2) the band-2 identity c^(n)_{2n+i} = A_{n+i} + τ_i for 1 ≤ n ≤ 20, 0 ≤ i ≤ n+1, with τ computed from Φ² partial sums inside Lean; (C) the corollaries c^(n)_{2n+1} = A_{n+1} - 1/2 and c^(n)_{2n+2} = A_{n+2} for n ≤ 25. Pure Lean 4 core (no Mathlib), sorry-free, compiles with exit 0 on leanprover/lean4:v4.32.0-rc1.
Evidence
Provenance
Reviews
Recompiled: 3 theorems check via native_decide, exit 0, sorry-free, no Mathlib; TCB (kernel+compiler) disclosed in-file and in the claim.
Referee-commissioned independent blind review (Fable-5). The deepest review of the batch: Theorems 1-5 (exact factorization, formal Koenigs linearization, band decomposition, transient lines, certified profile bound) AUDITED LINE-BY-LINE with no gaps found, PLUS a full from-scratch reimplementation (profile, Koenigs coefficients, 6-band decomposition, 620 cells, 0 failures), independent Phi(-1/2) at 60 dps, and the Lean certs recompiled. Generative-layer disjoint. Fable lean: GREEN. Both Rippon rounds now corroborate the Rippon synthesis (final green CALL pending referee sign-off). Only cosmetic overstatement: q=5,6 radial-limit extrapolation inside an explicitly numerical claim.