step_e_mu
plain-language theorem explainer
step_e_mu supplies the coefficient for the electron-to-muon mass step as the passive-edge count plus the spherical-geometry term minus the quadratic alpha correction. Lepton-mass derivations in the Recognition framework cite it for the first rung of the generation ladder. It is realized by direct assignment of the fixed expression using the imported E_passive constant.
Claim. The electron-to-muon step is defined by $step_{e→μ} = E_{passive} + 1/(4π) - α²$, where $E_{passive}$ is the count of passive field edges.
background
The lepton generations module isolates core mass-step coefficients to break import cycles in the T10 derivations. E_passive is defined upstream as the passive edge count 12 - 1 = 11 via passive_field_edges D. The term 1/(4π) encodes the spherical geometry attached to those edges, while α² supplies the quadratic radiative correction.
proof idea
One-line definition that directly assigns the expression (E_passive : ℝ) + 1/(4 * Real.pi) - α² using the imported passive-edge constant and the fine-structure constant.
why it matters
This definition is referenced by the O4 channel closure certificate and the step_e_mu_channel_split theorem in JCostPerturbation, which bundle it with the muon-to-tau step to certify canonical slots. It supplies the first link in the lepton chain, driven by the 11 passive edges and 1/4π geometry, and supports the mass formula on the phi-ladder by fixing the base transition coefficient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.