jcost_two_channel_coeff
plain-language theorem explainer
This definition selects the unique real coefficient completing the cubic term in the expansion of twice the J-cost at one plus the fine-structure constant. Mass-spectrum derivations in Recognition Science cite it to close the O4 perturbative channel. The construction is a one-line wrapper that invokes classical choice on the existence witness from the upstream uniqueness theorem.
Claim. Let $c$ be the unique real number such that $2J(1+α)=α^2 + c α^3$, where $J$ is the J-cost function and $α$ is the fine-structure constant.
background
The module supplies the mass-layer bridge for J-cost perturbations and certifies the O4 perturbative closure. The J-cost function assigns a recognition cost to each state, with the identity event at state 1 carrying zero cost. The doubled-channel identity expands twice this cost at argument 1+α into a quadratic leading term plus a cubic correction whose coefficient is isolated here.
proof idea
The definition is a one-line wrapper. It applies classical choice to the existence part of the unique-existence theorem for the cubic coefficient in the doubled J-cost channel.
why it matters
The coefficient supplies the explicit constant required to close the cubic-channel form of the Jcost(1+α) expansion. It is invoked by the specification theorem that verifies the identity and by the iff theorem that characterizes any solution as equal to this canonical choice. In the framework it completes the O4 coefficient forcing step that feeds lepton mass ratios and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.