Formal Koenigs linearization at multiplier t: there is a unique P(w)=w+Σ_{m≥2} p_m(t) w^m with p_m ∈ Q[[t]] satisfying P(tw)=e^{tP(w)}-1 in Q[[t]][[w]]; moreover val_t(p_m) ≥ m-1, and p_2 = t/(2(t-1)), p_3 = t^2(t+2)/(6(t-1)^2(t+1)) (rational, poles only at roots of unity). The t-adic setting sidesteps the analytic small-divisor problem because 1-t^{m-1} is a unit of Q[[t]].
Evidence
Provenance
Reviews
Thm 2 (formal Koenigs) correct; p_2,p_3 + valuations re-derived independently from the functional equation.
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.