step_e_mu_channel_split
plain-language theorem explainer
The electron-to-muon step decomposes as the passive edge contribution plus the fixed inverse-pi geometric term minus the quadratic correction. Lepton mass modelers cite this to anchor the canonical O4 channel form before radiative refinements. The proof is a direct simplification that unfolds the definitions of step_e_mu and correction_order_2.
Claim. The electron-to-muon step satisfies $step_{eμ} = E_{passive} + 1/(4π) - correction^{(2)}$.
background
In the Mass-Layer J-Cost Perturbation Bridge, the module certifies O4 perturbative closure by tying lepton steps to canonical forms. E_passive is the passive edge count defined as passive_field_edges D (equal to 11). step_e_mu is the base electron-muon transition from LeptonGenerations.Defs. correction_order_2 is the quadratic term from MassTopology. Upstream, canonical supplies the realization-independent arithmetic object, while forces encodes the magnitude-of-mismatch comparison.
proof idea
One-line wrapper that applies simp to unfold step_e_mu and correction_order_2, yielding the explicit split into passive edge, inverse-pi, and quadratic channel terms.
why it matters
This supplies the zeroth-order geometric channel for the e→μ step in the O4 closure. It is invoked directly by o4_channel_closure_certificate (which packages refined_shift together with both generation steps) and o4_slot_forcing_certificate (which forces the integer slots). The identity closes the coefficient forcing path for the lepton mass ladder inside the J-cost perturbation framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.