step_e_mu_invpi_quadratic_forced
plain-language theorem explainer
The theorem shows that in the mixed e-to-mu family written as E_passive plus one over k pi minus q times the second-order correction, the inverse-pi channel equality to one over four pi forces both k equals four and q equals one. Lepton mass modelers in the Recognition Science framework cite it when fixing the first-generation perturbative coefficients under spherical geometry. The proof reduces the channel match to k equals four by cross-multiplication and pi cancellation, then substitutes to invoke the quadratic scale forcing lemma for q.
Claim. Let $k$ be a positive integer and $q$ a real number. If the inverse-π channel satisfies $1/(kπ)=1/(4π)$ and the electron-to-muon step equals $E_mathrm{passive} + 1/(kπ) - q C^{(2)}$, then $k=4$ and $q=1$, where $E_mathrm{passive}$ is the passive edge count and $C^{(2)}$ denotes the second-order mass correction.
background
In the JCostPerturbation module the electron-to-muon step is the canonical expression $E_mathrm{passive} + 1/(4π) - α^2$, with $E_mathrm{passive}$ the passive-field edge count (11) drawn from the mass topology. The module supplies the generalized mixed-family form $E_mathrm{passive} + 1/(kπ) - q C^{(2)}$ and certifies its J-cost perturbative channel structure together with the explicit α² + 12α³ radiative decomposition. Upstream, the quadratic-scale-forced lemma already shows that the fixed 1/(4π) channel forces q=1; the magnitude-of-mismatch and universal-forcing-self-reference structures supply the single-valued comparison and orbit-coherence axioms that underwrite the channel match.
proof idea
Positivity lemmas establish that both kπ and 4π are nonzero. The channel equality is rewritten via div_eq_div_iff as the product identity (kπ)=4π. Multiplication by the reciprocal of π then yields k=4 by Nat.cast_inj. Substitution of this value into the step hypothesis produces the canonical quadratic form, to which the quadratic-scale-forced lemma is applied directly to obtain q=1. The two conclusions are packaged as a conjunction.
why it matters
The result supplies the inverse-π forcing half of the mixed-family closure for the e→μ step and is invoked by the full mixed-family theorem that additionally enforces the passive count s=E_passive. It completes the O4 perturbative coefficient package described in the module documentation for the J-cost perturbation bridge. Within the Recognition Science chain it fixes the first lepton-rung correction consistent with the eight-tick octave and D=3, supporting the mass formula on the phi-ladder; the companion no-hk variant removes the explicit positivity hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.