m_Z_exp_sigma
plain-language theorem explainer
Literal PDG-style 1σ uncertainty on the Z-boson mass, fixed at 2.1 (MeV in this module’s units). Mass-comparison and residual-band code cites it when checking RS φ-ladder predictions against experiment. The body is a bare real constant, not a derived claim.
Claim. The experimental one-standard-deviation uncertainty assigned to the $Z$ boson mass in the comparison tables is the real number $2.1$ (MeV).
background
Module Verification.MassComparison is quarantined from the certified RS surface: it imports PDG 2024 experimental central values and uncertainties, then compares them to RS mass predictions of the form $m = \mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$.
Sibling constants follow the same pattern (m_e_exp_sigma, m_mu_exp_sigma, quark and lepton bands, etc.): each *_exp is a measured central mass and each *_exp_sigma is the corresponding 1σ width used to form residuals or pull statistics.
The name collisions with ledger mass in the SevenGaps gravity development are unrelated; those define column or class mass on discrete ledgers, not particle rest masses.
proof idea
Definitional abbreviation: the real literal 2.1 is assigned with no proof obligations, lemmas, or tactics. No upstream theorem is applied.
why it matters
Supplies the experimental error bar against which an RS Z-mass (or nearby electroweak) prediction would be scored inside the quarantined comparison layer. It does not itself encode the φ-ladder, yardstick, or rung arithmetic; those live in Masses.Anchor and the sector geometry. With empty used_by in the current graph, it is infrastructure for residual tables rather than a step in the T0–T8 forcing chain. PDG 2024 is the external reference named in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.