mass_mu_MeV
plain-language theorem explainer
The declaration supplies the observed muon mass in MeV as the fixed real 105.6583755 drawn from CODATA 2022. Researchers verifying the T10 lepton ladder cite this value when comparing the phi-ladder prediction against experiment. It is introduced as a direct numeric definition with no internal derivation or lemmas.
Claim. The muon mass is defined by the constant $m_μ = 105.6583755$ MeV.
background
This definition sits inside the T10 Lepton Generations module, whose module documentation states that definitions are separated from theorems to break import cycles. The value serves as the experimental target for the electron-to-muon step on the lepton ladder, where the step is computed from passive edges, cube faces, wallpaper groups, and the fine-structure constant. The module imports structural mass, phi support, and alpha derivation from prior T6 and T9 results.
proof idea
The declaration is a direct numeric binding of the identifier to the literal real 105.6583755. No lemmas are applied and no tactics are invoked; the definition functions solely as a constant anchor for later interval propagation and relative-error checks in downstream theorems.
why it matters
The constant anchors the verification of the lepton ladder forced from T9. It is referenced in muon_mass_pred_bounds to place the predicted mass inside (105, 107) and in lepton_ladder_forced_from_T9 to confirm that the passive-field step reproduces the observed value within 2 percent relative error. The placement supports the claim that muon mass follows from cube geometry, wallpaper groups, and alpha without extra parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.