m_u_exp_sigma
plain-language theorem explainer
Numeric experimental one-sigma uncertainty on the up-quark mass, fixed at 0.49 MeV for PDG 2024 comparison. Anyone auditing RS φ-ladder mass predictions against data cites this constant as the error bar on m_u. It is a bare real assignment with no proof obligations.
Claim. The experimental one-sigma uncertainty on the up-quark mass is fixed as $\sigma(m_u^{\mathrm{exp}}) = 0.49\,\mathrm{MeV}$ (PDG 2024 scale, MS-bar convention).
background
The MassComparison module holds a quarantined side-by-side of Recognition Science mass predictions and PDG 2024 values. It is kept off the certified surface because it imports external experimental numbers and because the RS side still depends on the anchor/φ-ladder rung system.
RS masses take the form $m = \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. On the experimental side the module stores central values and one-sigma widths for leptons and light quarks so that residual comparisons can be stated as ordinary real inequalities.
m_u_exp_sigma is the uncertainty companion to the up-quark central value. Name collisions with ledger ``mass'' definitions in the SevenGaps gravity development are incidental; those objects count absolute debit/credit columns and play no role here.
proof idea
Pure definition: the real constant is set to the literal $0.49$. No lemmas, tactics, or reduction steps.
why it matters
Supplies the experimental error bar needed when the module compares the RS up-quark φ-ladder prediction to PDG 2024. Without a fixed $\sigma$, residual or band statements for $m_u$ cannot be written as concrete inequalities. Downstream use is currently empty in the graph, so the constant is infrastructure for the comparison table rather than an input to a named parent theorem. It sits entirely on the empirical side of the quarantine wall and does not touch T5–T8, RCL, or the derived constants $c$, $\hbar$, $G$, $\alpha$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.