m_t_exp_sigma
plain-language theorem explainer
Fixes the PDG-side 1σ uncertainty on the top-quark mass at 290 MeV for the RS-versus-experiment mass table. Anyone auditing lepton/quark mass residuals in Verification.MassComparison cites this constant as the experimental error bar. The body is a bare real literal; no proof.
Claim. The experimental one-standard-deviation uncertainty on the top-quark mass, in MeV, is the constant $290$.
background
Module Verification.MassComparison is a quarantined comparison layer: it juxtaposes Recognition Science mass predictions against PDG 2024 central values and errors. It is kept off the certified surface because experimental numbers are imported, not derived, and because the RS side still depends on the φ-ladder anchor system.
RS masses take the form $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. Sibling constants in this file supply the matching experimental central values and sigmas for $e,\mu,\tau,u,d,s$ and the remaining quarks; m_t_exp_sigma is the top-quark error entry in that table.
Graph edges that point at unrelated ledger mass and witness W structures are name collisions, not mathematical dependencies of this constant.
proof idea
Definitional abbreviation: the real is set equal to the literal 290. No lemmas, no tactics, no reduction.
why it matters
Supplies the experimental denominator for top-quark residual checks (prediction minus PDG central value, in units of this sigma). Together with the matching central-value constant it lets the module report how many experimental standard deviations separate the RS φ-ladder mass from PDG 2024. It does not itself touch the forcing chain (T5–T8), the Recognition Composition Law, or the mass-yardstick derivation; it is pure comparison infrastructure. No downstream theorems currently record a use edge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.