step_e_mu_invpi_scale_forced
plain-language theorem explainer
The theorem forces the inverse-pi scale factor in the electron-muon mass step to equal exactly 4 whenever the expression matches the canonical passive-edge form. Researchers closing lepton mass ratios inside the Recognition Science J-cost perturbation framework would cite this result when completing the O4 coefficient forcing. The proof substitutes the channel-split identity, equates the fractional terms by linear arithmetic, and cancels the common pi factor via nonlinear arithmetic on the reals.
Claim. Assume $c > 0$ and that the electron-muon step satisfies $step_{eμ} = E_{passive} + 1/(c π) - δ^{(2)}$. Then necessarily $c = 4$.
background
The module supplies the mass-layer J-cost perturbation bridge that certifies the perturbative channel form for Jcost(1+α) together with the explicit α² + 12α³ radiative decomposition. E_passive is the passive edge count abbrev defined as 12 - 1 = 11. The sibling step_e_mu_channel_split supplies the canonical decomposition of the step into the passive term plus 1/(4π) minus the second-order correction.
proof idea
The proof first applies step_e_mu_channel_split to obtain the canonical expression carrying denominator 4π. It then uses linarith on the two expressions for step_e_mu to equate the fractional terms 1/(cπ) and 1/(4π). Positivity lemmas establish both denominators are nonzero; nlinarith followed by mul_right_cancel then yields c = 4.
why it matters
This supplies the scale-forcing step that the downstream theorem step_e_mu_full_real_family_forced_from_passive_term builds upon to obtain the full real-family forcing. It closes the inverse-pi component of the O4 perturbative closure in the mass layer, consistent with the eight-tick octave and phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.