step_e_mu_quadratic_scale_forced
plain-language theorem explainer
In the Recognition Science lepton mass ladder the electron-muon step takes the perturbative form E_passive plus one over four pi minus q times alpha squared. Canonical matching in this quadratic channel forces the coefficient q to equal one. The proof obtains the canonical expression via channel split, equates the quadratic terms by linear arithmetic, and cancels the nonzero alpha-squared factor using right-multiplication.
Claim. If $step_{eμ} = E_{passive} + 1/(4π) - q α²$, then $q = 1$.
background
The JCostPerturbation module upstreams the O4 perturbative closure into the Masses namespace and ties it to canonical lepton-step definitions. It certifies the Jcost(1+α) perturbative channel form and the explicit α² radiative decomposition used in refined_shift. E_passive is the passive edge count 11. correction_order_2 is the quadratic term α². step_e_mu_channel_split supplies the canonical expression for the electron-muon step without the q factor. alpha is the fine-structure constant defined as one over alphaInv.
proof idea
The proof first invokes step_e_mu_channel_split to obtain the canonical form step_e_mu = E_passive + 1/(4π) - correction_order_2. Linear arithmetic then yields q * correction_order_2 = correction_order_2. Alpha bounds establish alpha > 0 hence nonzero, so correction_order_2 = α² is nonzero. After rewriting the product as one times the term, right-multiplication cancellation gives q = 1.
why it matters
This result closes the quadratic scale in the e-mu family and feeds the equivalence theorems step_e_mu_denominator_iff_quadratic_scale and step_e_mu_invpi_quadratic_forced. It realizes the joint forcing of denominator and quadratic slots under canonical matching, consistent with the J-cost composition law and the phi-ladder mass formula. It contributes to the O4 coefficient forcing closure in the Recognition Science mass spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.