step_e_mu_scale_iff_passive_term_no_hc_pos
plain-language theorem explainer
The equivalence links the inverse-pi denominator scale to the passive edge count in the electron-muon mass step under the O4 perturbation ansatz. Researchers deriving lepton masses from J-cost channels in Recognition Science cite it to confirm canonical matching without positivity hypotheses. The proof splits into forward and reverse directions, applying the fixed channel split for one direction and the inverse-pi forcing lemma for the other.
Claim. Let $s, c$ be real numbers. Suppose the electron-muon step satisfies $step_{eμ} = s + 1/(c π) - α²$. Then $c = 4$ if and only if $s = E_{passive}$.
background
In the J-cost perturbation framework the electron-to-muon step is expressed as a sum of a passive geometric term, an inverse-pi channel, and a quadratic correction. The module bridges mass-layer perturbations to canonical lepton definitions by certifying coefficient forcing in the O4 closure. Upstream, the channel split fixes the inverse-pi term at 1/(4π) with the passive count, while the inverse-pi forcing lemma derives the scale 4 when the passive term matches E_passive.
proof idea
The proof uses a constructor to establish the biconditional. For the forward direction, substitute c=4 into the hypothesis and apply linarith with the channel split lemma. For the reverse, substitute the passive equality and invoke the inverse-pi scale forcing theorem directly.
why it matters
This packages the positivity-free equivalence for the e→μ real-scale matching, feeding directly into the bundled lepton scale iff statement that combines e→μ and μ→τ sectors. It fills the O4 coefficient forcing step in the mass perturbation bridge, confirming the denominator scale 4 matches the passive edge count without extra assumptions. In the Recognition framework it supports the phi-ladder mass formulas by locking the geometric constants in the lepton generations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.