step_e_mu_invpi_quadratic_forced_no_hk
plain-language theorem explainer
The theorem shows that matching the inverse-pi channel term exactly to 1/(4 pi) inside the mixed electron-muon step expression E_passive + 1/(k pi) - q alpha squared forces the integer k to 4 and the quadratic coefficient q to 1. Lepton-mass workers in Recognition Science cite it to close the O4 perturbative coefficients for the mixed family without a separate positivity hypothesis on k. The proof first derives a contradiction from the k = 0 case using the channel equality and then reduces directly to the prior quadratic-forcing lemma.
Claim. Assume $1/(k pi) = 1/(4 pi)$ and step$_{e mu} = E_{passive} + 1/(k pi) - q alpha^2$. Then $k = 4$ and $q = 1$.
background
The result lives inside the Mass-Layer J-Cost Perturbation Bridge module, which upstreams the O4 perturbative closure and links it to canonical lepton-step definitions. The module certifies the Jcost(1+alpha) perturbative channel form together with the explicit alpha squared plus 12 alpha cubed radiative decomposition. Local objects include the electron-muon step value, the passive energy term, and the second-order correction proportional to alpha squared.
proof idea
The tactic proof opens with a case split on k = 0. The zero case produces an immediate contradiction because the channel hypothesis would force 0 = 1/(4 pi), which is positive. For the nonzero case it obtains k > 0 from Nat.pos_of_ne_zero and then applies the upstream lemma step_e_mu_invpi_quadratic_forced to finish the proof.
why it matters
This supplies the positivity-free route for mixed e to mu forcing and is invoked by the downstream full mixed-family closure theorem step_e_mu_full_mixed_family_forced_from_passive_and_channel_no_hk. It completes the O4 coefficient forcing step inside the JCostPerturbation module. In the Recognition framework it fixes the quadratic correction on the phi-ladder mass formula without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.