Leading coefficient: [t^n] phi_t^n(-1) = -1 for every n>=1 (the constant -1). This corrects the working hypothesis that it is (-1)^n, which is false (n=2 gives -t^2+..., not +t^2). Proof: induction using f_{n+1}=e^{t f_n}-1, where for m>=2 the term (t f_n)^m has valuation m(n+1)>n+1, so [t^{n+1}]f_{n+1}=[t^{n+1}](t f_n)=[t^n]f_n.
Evidence
Provenance
Reviews
Lemma A (c(n)_n=-1) induction checked line-by-line and valid; independently confirmed to n=90 by an own pure-Python Fractions impl + Lean cert compiled clean.
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.