step_e_mu
plain-language theorem explainer
step_e_mu defines the electron-to-muon mass step as the passive edge count plus the spherical term 1/(4π) minus the quadratic alpha correction. Researchers deriving lepton masses in the Recognition Science framework cite this definition when assembling the generation chain from geometric primitives. The definition is assembled directly from the upstream E_passive count and the fine-structure constant without further reduction.
Claim. The electron-to-muon generation step is given by $s_{eμ} = E_{passive} + 1/(4π) - α²$, where $E_{passive}$ is the passive edge count in three-dimensional space.
background
The module supplies core definitions for lepton mass derivations under the T10 heading, separating them from theorems to avoid import cycles. E_passive is defined as the passive edge count passive_field_edges 3, equivalently 12 - 1 = 11. The spherical geometry term 1/(4π) enters as the leading geometric factor for the electron-muon transition.
proof idea
Direct definition that substitutes the upstream E_passive abbreviation and the explicit constants 1/(4 * Real.pi) and α² into the expression for the step.
why it matters
This definition supplies the canonical e→μ form required by downstream results such as o4_channel_closure_certificate and lepton_integer_slot_iff_bundle_no_hk in JCostPerturbation. It fills the first half of the T10 lepton generations definitions and supplies the geometric input for the mass ladder. It connects to the Recognition Science mass formula via the passive-edge count but does not yet incorporate phi-ladder rung adjustments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.