muon_mass_step_hypothesis
plain-language theorem explainer
The muon mass lies within a 2% relative error of the value predicted by the passive field step on the topological phi-ladder. Researchers modeling lepton mass hierarchies via generation steps would cite this when validating the electron-to-muon transition against CODATA data. The proof starts from the proven interval (105,107) for the prediction, subtracts the fixed experimental mass 105.6583755, and reduces the absolute bound to a relative one by division and numerical comparison.
Claim. Let $m_μ^{pred}$ be the muon mass predicted from the structural mass and φ-residue. Let $m_μ = 105.6583755$ MeV be the experimental value. Then $|m_μ^{pred} - m_μ| / m_μ < 2/100$.
background
The module derives lepton masses by extending the topological ladder from the electron. The mass in generation n satisfies $m_n = m_{struct} · φ^{Δ_n}$, with successive generations separated by topological steps $Δ_{n+1} = Δ_n + S_{n→n+1}$. For the electron-to-muon transition the passive field step is $S_{e→μ} = 11 + 1/(4π) - α² ≈ 11.07952$ (MODULE_DOC). Upstream, muon_mass_pred_bounds supplies the interval (105,107) for the predicted mass via interval propagation from structural_mass and φ-residue. The experimental anchor is fixed by the definition mass_mu_MeV = 105.6583755 MeV (CODATA 2022).
proof idea
The tactic proof invokes muon_mass_pred_bounds to obtain the interval, simplifies the experimental mass, applies abs_lt and linarith to bound the absolute difference by 2, confirms positivity of the mass, uses div_lt_div_of_pos_right to convert to a relative bound, and finishes with a calc block plus norm_num to compare 2/105.658 < 2/100.
why it matters
This result verifies the passive field step hypothesis for the first lepton generation transition in T10. It supplies the corresponding statement in the RRF.Physics.LeptonGenerations module. The verification supports the framework claim that masses arise from phi-ladder increments tied to the forcing chain (T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave). It touches the open question of whether refined interval propagation can reduce the 2% tolerance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.