m_u_exp
plain-language theorem explainer
Records the PDG 2024 experimental up-quark mass as the real constant 2.16 MeV (MS-bar at 2 GeV). Cited by mass-comparison checks that score Recognition Science φ-ladder predictions against external data. Pure numeric definition; no proof obligation.
Claim. The experimental up-quark mass is the real number $m_u^{\mathrm{exp}} = 2.16$ MeV, quoted in the $\overline{\mathrm{MS}}$ scheme at $2\,\mathrm{GeV}$, with the PDG uncertainty band $2.16(49)\,\mathrm{MeV}$ noted in the source comment.
background
The module MassComparison is quarantined from the certified RS surface: it imports PDG experimental numbers and compares them to RS mass predictions built on the φ-ladder. Predictions take the form $m(\mathrm{species}) = \mathrm{yardstick}(\mathrm{sector}) \times \varphi^{r_0 + r_{\mathrm{species}}}$, with yardstick fixed by coherence energy $E_{\mathrm{coh}} = \varphi^{-5}$ and sector integers from cube geometry.
Sibling constants (m_e_exp, m_d_exp, …) hold the corresponding PDG central values for leptons and other quarks. This entry is the up-quark datum only; the companion m_u_exp_sigma carries the uncertainty 0.49 MeV. Units are MeV throughout the comparison layer.
proof idea
No proof. The declaration is a one-line def binding the real literal 2.16 to the name used by downstream comparison lemmas. The parenthetical uncertainty in the doc-comment is documentary; it is not encoded in this constant.
why it matters
Supplies the external anchor against which RS up-quark mass predictions are scored inside the quarantined verification layer. Without fixed PDG numbers, residual and σ-level checks cannot be stated as Lean equalities or inequalities. It does not derive mass from the forcing chain (T0–T8) or the RCL; it only records the experimental side of the comparison. The module’s epistemological note is explicit: experimental imports stay off the certified surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.