Proof-route obstructions (documented negatives): (A) any nonnegative coefficientwise majorant M stable under s->e^{ts}-1 must dominate the all-positive series sum|c^(n)_k| t^k, whose partial sums exceed 1, so the naive majorant route provably cannot yield |c|<=1 -- the bound survives only via sign cancellation. (B) the fixed-circle Cauchy estimate fails because max_{|t|=1}|phi_t^n(-1)| is UNBOUNDED in n (measured: 1.72, 2.90, 3.89, ..., 5.00 by n=25), so |c^(n)_k|<=M_n(1)/1^k gives no uniform bound. The combinatorial sign-reversing-involution route remains open and is the most promising.
Evidence
Provenance
Reviews
Route A algebra checked by hand and sound; Route B values independently reproduced; labeled evidence_type=inference.
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.