Rippon 7.54, round 2: Koenigs band decomposition of the coefficient array, the transient-line theorem, and a certified obstruction — the conjecture is equivalent to bounds on one hierarchy of universal power series

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)).

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]].

Band decomposition theorem: f_n = Σ_{m≥1} p_m(t) t^{mn} Φ(t)^m (t-adically), the m-th summand having valuation ≥ mn+m-1. Hence with Ψ_m := p_m Φ^m (universal series independent of n): c^(n)_k = Σ_{m(n+1)≤k+1} [t^{k-mn}] Ψ_m — a FINITE sum for every (n,k) — and Rippon's conjecture is EQUIVALENT to the family of inequalities |Σ_m [t^{k-mn}] Ψ_m| ≤ 1. This subsumes and supersedes the round-1 reduction: the transient region (II) is no longer unstructured; the iterate index n enters only through which band-profile coefficients are summed.

Transient-line theorem (bands 2 and 3): for all n≥1, c^(n)_{2n+i} = A_{n+i} + τ_i for 0≤i≤n+1, and c^(n)_{3n+i} = A_{2n+i} + τ_{n+i} + σ_i for 0≤i≤n+2, where τ_i = [t^i](p_2 Φ²) = -(1/2)Σ_{l<i}[t^l]Φ² and σ_i = [t^i](p_3 Φ³). Corollaries: c^(n)_{2n+1} = A_{n+1} - 1/2 and c^(n)_{2n+2} = A_{n+2} for ALL n≥1; the transient ridge c^(n)_{2n+1} → -1/2; and round-1's non-leading supremum 2663/4480 at (6,13) is explained exactly as |A_7 - 1/2| (A_7 = -423/4480 is the most negative profile term). On k ≤ 3n+1 the conjecture reduces to profile bounds: it would follow from |A_j| ≤ 1/2 (j≥1) and |τ_i| ≤ 1/2 with the observed strictness.

Analytic profile theorem: (a) the power series Φ has radius of convergence R ≥ ln 2 = 0.6931…, and on |t| ≤ ρ < ln 2 the entire functions t^{-n} f_n(t) converge uniformly to the sum of Φ (elementary majorant x_{k+1}=e^{ρ x_k}-1, decreasing to 0 exactly when ρ < ln 2); (b) for every real t ∈ (0,1) the orbit f_k(t) increases in (-1,0) to 0 and the Koenigs value G(t) = -∏_{k≥0} h(t f_k(t)) lies in (-1,0): the conjectured profile bound |Φ| ≤ 1 HOLDS on the whole positive real segment.

Certified obstruction: Φ(-1/2) ∈ [-1.1590440509550799, -1.1590440509550797] < -1 (note |−1/2| < ln 2 ≤ R, so this is the sum of the series itself). By the maximum principle, M(r) := max_{|t|=r} |Φ| ≥ 1.159 for EVERY r ∈ [1/2, R). Hence the Cauchy/sup-norm estimate |A_j| ≤ M(r) r^{-j} cannot prove statement (I) even in the limit r ↑ R: an Abel-type argument (M(r)→1) is ruled out — M(r) stays bounded away from 1. The |A_j| ≤ 1 phenomenon is strictly a cancellation phenomenon, not an L^∞ one, at the profile level (sharpening round-1's Route-B failure analysis into a rigorous statement).

Profile data, 600 exact terms (statement (I) survives a deeper probe; no counterexample): |A_j| ≤ 1 for all 0 ≤ j ≤ 600 in exact rational arithmetic, with max_{j≥1} |A_j| = 1/2 attained ONLY at j=1 and |A_j| < 1/2 for 2 ≤ j ≤ 600. Likewise the computed band profiles obey |τ_i| ≤ 1/2 (equality only at i=1; second largest 5/24) and |σ_i| ≤ 1/3 (equality only at i=2) for i ≤ 600, both tending to 0. Also |S_J| = |Σ_{j≤J} A_j| ≤ 1 with equality only at J=0 (the coefficients of Φ/(1-t) obey the same law).

Boundary picture (numerical, from 600 exact terms): |A_j|^{1/j} climbs to ≈0.990 and the envelope decays like j^{-0.88} (radius of convergence R = 1 conjectured); Φ satisfies NO P-recurrence of order ≤ 8 with polynomial coefficients of degree ≤ 12-order (guess_holonomic.py, exact arithmetic mod 2^61-1 with validation rows) — empirically not holonomic; radial limits at root-of-unity directions e^{2πip/q} (q ≤ 6) tend to 0, consistent with parabolic dynamics (f_n → 0 sub-geometrically at |t|=1 parabolic parameters, so t^{-n}f_n → 0), suggesting a dense set of boundary zeros and a NATURAL BOUNDARY at |t|=1 (which would explain non-holonomicity); Φ(r)/(1-r) → ≈ -2 (simple zero at 1, matching the classical parabolic orbit rate f_k(1) ~ -2/k); and the L¹ circle means (1/2π)∫|Φ(re^{iθ})|dθ lie in [1.02, 1.13] for r ∈ [0.5, 0.985] — the Hardy H¹ route is also obstructed numerically, though by the smallest margin (~2-13%) of any classical route tried.

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.