jcost_two_channel_coeff_spec
plain-language theorem explainer
The canonical coefficient in the doubled J-cost expansion for the fine-structure perturbation satisfies the exact identity 2 Jcost(1 + α) = α² + c α³. Mass-layer calculations in Recognition Science cite this result when closing the O4 perturbative coefficient forcing. The proof is a term-mode wrapper that extracts the witness from the upstream uniqueness theorem via classical choice and matches it to the canonical definition.
Claim. Let $J$ be the J-cost function and let $c$ be the canonical cubic coefficient. Then $2 J(1 + α) = α^2 + c α^3$, where $α$ is the fine-structure constant.
background
The Mass-Layer J-Cost Perturbation Bridge module certifies the perturbative channel form for Jcost(1 + α) and ties it to canonical lepton-step definitions. J-cost is the recognition cost function whose minimum occurs at the identity event (state = 1). The fine-structure constant α is introduced as 1/α_inv in the Constants.Alpha module.
proof idea
Term-mode proof. It applies ExistsUnique.exists to the upstream uniqueness theorem jcost_two_channel_coeff_unique to obtain an existence witness for the cubic coefficient, then uses Classical.choose_spec to recover the canonical value defined by jcost_two_channel_coeff.
why it matters
This theorem certifies the explicit cubic coefficient used in the O4 perturbative closure. It directly feeds the downstream characterization theorem jcost_two_channel_coeff_iff, which states that any real number satisfying the doubled-channel identity equals the canonical coefficient. In the Recognition framework the result closes the α² + c α³ radiative decomposition required for refined_shift and the mass-layer bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.