Exact factorization theorem: with f_0=-1, f_{n+1}=e^{t f_n}-1 and h(x)=(e^x-1)/x, every iterate factors as f_n = -t^n ∏_{k=0}^{n-1} h(t f_k(t)) in Q[[t]]; consequently the stable profile is the t-adically convergent infinite product Φ = -∏_{k≥0} h(t f_k), and diagonal stabilization (round-1 Lemma B, threshold n≥j) follows anew. Proof: proofs/proofs2.md §1 (one-line induction from e^x-1 = x·h(x)).
Evidence
Provenance
Reviews
Thm 1 (exact factorization) proof correct (induction + t-adic Cauchy); independently reproduced, 0 failures.
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.