m_t_exp
plain-language theorem explainer
Experimental top-quark rest mass from PDG 2024, stored as the real constant 172570 MeV (central value 172.57 GeV). Mass-comparison and verification code cites it as the laboratory anchor against which Recognition Science ladder predictions are scored. The body is a bare numeric definition with no proof obligations.
Claim. The PDG 2024 central value of the top-quark mass is fixed at $m_t^{\mathrm{exp}} = 172570\,\mathrm{MeV}$ (equivalently $172.57\,\mathrm{GeV}$, with reported uncertainty $290\,\mathrm{MeV}$).
background
The enclosing module compares Recognition Science mass predictions to PDG 2024 laboratory values. It is quarantined from the certified surface because it imports external experimental numbers and because the RS side still depends on the anchor/yardstick system on the $\varphi$-ladder.
RS predicts a species mass by $m(\mathrm{species})=\mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$ and sector integers fixed by cube geometry. Experimental anchors such as this top-quark entry supply the denominator (or difference) in those comparisons.
Sibling constants in the same file hold the electron, muon, tau, and light-quark experimental masses in the same MeV convention.
proof idea
Pure definition: the real constant is assigned the literal decimal 172570. No lemmas, tactics, or reduction steps are involved.
why it matters
Supplies the laboratory top-quark mass used when the verification layer scores RS $\varphi$-ladder predictions against PDG 2024. The module formula $m=\mathrm{yardstick}\times\varphi^{r_0+r}$ is the same mass ladder that appears throughout Recognition Science (yardstick built from $E_{\mathrm{coh}}=\varphi^{-5}$ and sector integers). Without a fixed experimental anchor the residual or sigma comparison for the top cannot be stated. The declaration itself carries no theorem content; it only freezes the PDG central value so downstream comparison lemmas remain reproducible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.