step_e_mu
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute numerical muon or tau masses.
- Does not derive E_passive from a deeper axiom.
- Does not include the muon-to-tau step coefficient.
- Does not incorporate corrections beyond order α².
formal statement (Lean)
37noncomputable def step_e_mu : ℝ :=
proof body
Definition body.
38 (E_passive : ℝ) + 1 / (4 * Real.pi) - α ^ 2
39
40/-- Step 2: Muon to Tau.
41 Driven by Faces (6) and Wallpaper Symmetry (17).
42 Coefficient: W + D/2 = (2W + D)/2. -/
used by (40)
-
lepton_integer_slot_iff_bundle_no_hk -
lepton_real_scale_iff_bundle_no_hc_pos -
o4_channel_closure_certificate -
o4_slot_forcing_certificate -
step_e_mu_channel_split -
step_e_mu_denominator_iff_quadratic_scale -
step_e_mu_denominator_iff_quadratic_scale_no_hk -
step_e_mu_full_family_forced_from_channel_match -
step_e_mu_full_family_forced_from_channel_match_no_hk -
step_e_mu_full_family_forced_from_passive_term -
step_e_mu_full_family_forced_from_passive_term_no_hk -
step_e_mu_full_mixed_family_forced_from_passive_and_channel -
step_e_mu_full_mixed_family_forced_from_passive_and_channel_no_hk -
step_e_mu_full_mixed_family_forced_from_passive_and_quadratic_scale -
step_e_mu_full_mixed_family_forced_from_passive_and_quadratic_scale_no_hk -
step_e_mu_full_real_family_forced_from_passive_term -
step_e_mu_full_real_family_forced_from_passive_term_no_hc_pos -
step_e_mu_invpi_denominator_forced -
step_e_mu_invpi_denominator_forced_from_quadratic_scale -
step_e_mu_invpi_denominator_forced_from_quadratic_scale_no_hk -
step_e_mu_invpi_denominator_forced_no_hk -
step_e_mu_invpi_quadratic_forced -
step_e_mu_invpi_quadratic_forced_no_hk -
step_e_mu_invpi_scale_forced -
step_e_mu_invpi_scale_forced_no_hc_pos -
step_e_mu_passive_term_forced -
step_e_mu_quadratic_scale_forced -
step_e_mu_scale_iff_passive_term_no_hc_pos -
predicted_residue_mu -
gap_minus_shift_bounds_proven