mass_mu_MeV
plain-language theorem explainer
The declaration records the experimental muon mass of 105.6583755 MeV from CODATA 2022. Researchers verifying the T10 lepton ladder would cite this constant when checking predicted values against observation. It functions as a direct numerical assignment with no derivation steps.
Claim. The observed muon mass equals 105.6583755 MeV.
background
The T10 Lepton Generations Definitions module isolates numerical constants to break import cycles with necessity theorems. This entry supplies the observed muon mass for interval comparisons against the predicted value obtained from the electron structural mass plus the step factor.
proof idea
The declaration is a direct definition that assigns the numerical value 105.6583755 with no lemma applications or computational steps.
why it matters
This constant anchors verification that the muon mass follows the passive field step. It is referenced by muon_mass_pred_bounds to establish the interval (105, 107) and by lepton_ladder_forced_from_T9 to confirm the T10 result that the ladder is forced from T9 via passive edges, cube faces, wallpaper groups, and the fine-structure constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.