m_c_exp_sigma
plain-language theorem explainer
Fixed experimental 1σ uncertainty on the charm-quark mass, set to 20 MeV from PDG 2024. Used only inside the quarantined mass-comparison tables that score RS φ-ladder predictions against measured values. The body is a literal real constant; there is no proof obligation.
Claim. The PDG experimental one-standard-deviation uncertainty on the charm-quark mass is $\sigma(m_c)=20\,\mathrm{MeV}$.
background
The module MassComparison scores Recognition Science mass predictions against PDG 2024 numbers. It is quarantined from the certified surface because it imports external experimental data and because the predictions sit on the anchor/φ-ladder system.
RS masses take the form $m=\mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r}$, with yardstick built from the coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$ and sector integers from cube geometry. For each species the module stores a central experimental value and a matching 1σ width; this declaration is the width for charm.
Upstream name collisions on mass (ledger column mass, class mass in the SevenGaps posting layer) are unrelated: they measure discrete ledger weight, not particle rest mass.
proof idea
Pure definitional assignment: the real constant is written as the numeral 20. No lemmas, tactics, or reduction steps.
why it matters
Supplies the experimental error bar against which an RS charm-mass prediction would be judged inside this verification module. It does not itself derive a mass; it only records the PDG uncertainty so residual or σ-score computations can be stated. The module sits outside the forcing chain (T0–T8) and outside the certified surface; no downstream theorems currently consume the constant (used_by is empty). It is bookkeeping for the paper-level claim that ladder masses land inside PDG bands.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.