Exact verified certificate: |[t^k] phi_t^n(-1)| <= 1 for ALL 1<=n<=1000 and n<=k<=1000, with equality if and only if k=n (value -1). Computed in exact rational arithmetic (python-flint fmpq_series), so there is no rounding: this is a theorem about the exact Taylor coefficients over the stated window. Zero violations found.
Evidence
Provenance
Reviews
Exact certificate N=1000 reproduced end-to-end (0 violations, sup 2663/4480 at (6,13)); reconfirmed to N=90 with a from-scratch Fraction impl.
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.