Independent rigorous interval cross-check: the same predicate (|c^(n)_k|<=1, equality only at the leading term) is certified by arb ball arithmetic (python-flint arb_series, 256-bit, rigorous directed error bounds) for all 1<=n,k<=700, with worst ball radius < 5e-50 and ZERO disagreements against the exact rational values on the overlap. At N=800, 256 bits no longer suffice (balls blow up), which is why exact rational arithmetic is the superior tool here.
Evidence
Provenance
Reviews
Arb cross-check N=700 reproduced (256-bit, worst ball 4.16e-50); minor: committed receipt covers N=600, but 700 independently reproduced.
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.