m_mu_exp
plain-language theorem explainer
Experimental muon rest mass fixed at 105.6583755 MeV (PDG 2024 central value). Mass-verification and lepton-ratio theorems cite it as the denominator and comparison target for RS phi-ladder predictions. Bare real constant; no derivation.
Claim. The PDG 2024 central value of the muon rest mass is $m_\mu^{\mathrm{exp}} = 105.6583755\,\mathrm{MeV}$.
background
The MassComparison module is quarantined from the certified RS surface: it imports external PDG numbers and compares them to phi-ladder mass predictions. Those predictions take the form $m(\mathrm{species}) = \mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$ and sector integers fixed by cube geometry.
Sibling constants supply the electron and tau experimental masses (and their sigmas). The muon entry here is the central value only; the parenthetical uncertainty $(23)$ in the doc-comment is not encoded in the real.
Upstream, the same numeric literal appears in Masses.Verification as the shared experimental anchor for lepton checks.
proof idea
Definitional constant: the real is assigned the decimal 105.6583755 with no proof obligations, lemmas, or tactics.
why it matters
Feeds the muon arm of the mass-verification certificate (muon_in_range, muon_pct) and the relative-error theorem that bounds $|m_{\mathrm{RS}}(\ell=13)-m_\mu^{\mathrm{exp}}|/m_\mu^{\mathrm{exp}}<0.04$. Also enters phi_ladder_verified (interval check that the empirical-electron-anchored ladder meets percent-level PDG tolerances) and the experimental muon-to-electron ratio used for ratio bounds near 206.76–206.77.
In the broader RS picture this is pure external data: the framework’s mass formula (yardstick times phi-rung) is tested against it, not derived from it. The module’s quarantine note makes that epistemological split explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.