jcost_two_channel_form
plain-language theorem explainer
The theorem certifies existence of a real coefficient c such that twice the J-cost at one plus the fine-structure constant expands as alpha squared plus c times alpha cubed, with absolute value of c at most four. Mass derivations in Recognition Science cite this to close the O4 perturbative channel before invoking ledger fractions or topology counts. The proof is a direct one-line application of the two_jcost_one_plus_alpha_expansion lemma.
Claim. There exists a real number $c$ such that $2 J(1 + α) = α² + c α³$ and $|c| ≤ 4$, where $α$ is the fine-structure constant and $J$ denotes the J-cost function.
background
The J-cost function is the Recognition Science cost measure built from the J-uniqueness map J(x) = (x + x⁻¹)/2 - 1 that satisfies the Recognition Composition Law. The module Mass-Layer J-Cost Perturbation Bridge upstreams the O4 perturbative closure, certifying both the Jcost(1+α) channel form and the explicit α² + 12α³ radiative decomposition used in refined_shift. Alpha is defined as the reciprocal of alphaInv; Cost is the abbrev for Quantity CostUnit.
proof idea
The proof is a one-line wrapper that applies the two_jcost_one_plus_alpha_expansion lemma to obtain the cubic channel form together with the coefficient bound.
why it matters
This supplies the certified perturbative channel form that the sibling results on mass topology counts and ledger fractions rely upon. It closes the O4 coefficient forcing step described in the module documentation and sits inside the alpha band (137.030, 137.039) of the Recognition Science constants. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.