jcost_two_channel_coeff_iff
plain-language theorem explainer
The equivalence states that a real coefficient c satisfies the doubled J-cost expansion 2 Jcost(1 + alpha) equals alpha squared plus c alpha cubed precisely when c matches the canonical two-channel coefficient. Researchers closing O4 perturbative mass corrections in the Recognition Science framework cite this to enforce uniqueness of the cubic term. The proof is a term-mode biconditional split that invokes the cubic uniqueness lemma forward and the specification theorem backward.
Claim. Let $c$ be a real number. Then $2 J(1 + alpha) = alpha^2 + c alpha^3$ if and only if $c$ equals the canonical two-channel coefficient, where $J$ denotes the J-cost function and $alpha$ is the fine-structure constant.
background
The Mass-Layer J-Cost Perturbation Bridge module certifies the perturbative form of the J-cost evaluated at 1 plus the fine-structure constant. J-cost is the recognition cost drawn from the RS-native Cost quantity, which measures the functional cost of a given real input under the Recognition Composition Law. The doubled-channel identity isolates the cubic coefficient in the expansion of 2 Jcost(1 + alpha) as alpha squared plus that coefficient times alpha cubed.
proof idea
The term proof opens the biconditional with constructor. The forward direction applies the uniqueness lemma two_jcost_cubic_coeff_unique to the hypothesis that c satisfies the identity together with the specification theorem for the canonical coefficient. The reverse direction substitutes the equality into the specification theorem via simpa.
why it matters
This characterization closes the coefficient forcing step inside the O4 perturbative package for lepton masses. It supplies the exact uniqueness needed for the refined_shift and geometric evaluations of zeroth-order constants referenced in the module documentation. In the broader framework it anchors the alpha-dependent channel form that feeds mass-ladder formulas and the phi-ladder correction factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.