step_e_mu
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical muon mass in MeV.
- Does not include the muon-to-tau step.
- Does not apply phi-ladder rung or gap corrections.
- Does not incorporate radiative corrections beyond α².
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). -/
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 -
step_e_mu