m_mu_exp_sigma
plain-language theorem explainer
PDG 2024 one-sigma experimental uncertainty on the muon rest mass, fixed as the real constant 0.0000023. Cited by anyone comparing Recognition Science muon-ladder predictions to measured values in this quarantined verification module. The body is a literal numeric definition, not a derived claim.
Claim. The experimental standard uncertainty on the muon rest mass is the real number $0.0000023$, in the same energy units as the companion experimental central value used in this module.
background
The module Machine-Verified Mass Predictions Comparison holds PDG 2024 central values and uncertainties next to Recognition Science mass predictions. It is quarantined from the certified surface because experimental inputs are not RS-derived and because the predictions sit on the anchor and $\varphi$-ladder rung system.
RS masses 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 electron, muon, and tau experimental masses and sigmas (and light-quark analogues) for residual checks.
Name collisions with ledger mass in the SevenGaps gravity modules are irrelevant here: those count absolute debit/credit column totals as an induction measure. This declaration is only the PDG muon uncertainty numeral.
proof idea
Definitional constant: the real is assigned the literal decimal $0.0000023$. No lemmas, tactics, or algebraic reduction. The nearby doc line on the tau mass belongs to the next declaration, not this one.
why it matters
Gives the experimental error bar needed to score the RS muon mass against PDG 2024 (Navas et al.). Without $\sigma_\mu$, residual or pull comparisons in this verification layer cannot be stated. It sits with m_mu_exp and the other lepton/quark exp/sigma pairs; the module itself is deliberately off the certified surface. No downstream theorems currently depend on it in the graph. Framework landmarks touched only indirectly: the $\varphi$-ladder mass formula and anchor yardsticks that the comparison is meant to test, not this constant itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.