m_d_exp_sigma
plain-language theorem explainer
Literal PDG-style 1σ uncertainty on the down-quark mass, fixed at 0.48 (MeV scale used by the sibling central value). Cited only inside the quarantined mass-comparison tables that score RS φ-ladder predictions against experiment. The body is a bare real constant; no proof obligation.
Claim. The experimental one-standard-deviation uncertainty assigned to the down-quark mass in the PDG 2024 comparison tables is the real number $0.48$ (MeV, matching the sector units of the companion central-value constant).
background
The module Verification.MassComparison is explicitly quarantined from the certified RS surface: it imports external PDG 2024 numbers and the φ-ladder anchor system, neither of which is derived inside the forcing chain. Its job is a side-by-side numerical score of predicted versus measured masses.
RS masses themselves follow
$m(\mathrm{species})=\mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$,
with yardstick built from $E_{\mathrm{coh}}=\varphi^{-5}$ and sector integers from cube geometry. Experimental anchors sit beside those predictions as plain reals: a central value m_d_exp and this companion width m_d_exp_sigma.
Name collisions on mass in the SevenGaps gravity modules are unrelated ledger/column masses; they do not feed this constant.
proof idea
Definitional abbreviation: the real literal 0.48 is assigned directly. No lemmas, no tactics, no reduction.
why it matters
Supplies the experimental error bar against which the RS down-quark rung prediction is judged inside the quarantined comparison suite. Downstream use is currently empty in the graph, but the sibling pattern (m_e_exp_sigma, m_u_exp_sigma, …) shows the intended role: χ-style or interval checks of ladder masses versus PDG 2024. It does not touch T5–T8, RCL, or the certified forcing chain; it only documents the external datum the verification layer needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.