m_d_exp
plain-language theorem explainer
Experimental down-quark mass anchor used in the quarantined PDG comparison layer: 4.67 MeV in the MS-bar scheme at 2 GeV. Anyone checking RS quark-mass residuals against PDG 2024 cites this constant. It is a bare real literal, not a derived claim.
Claim. The PDG 2024 experimental down-quark mass (MS-bar at $2\,\mathrm{GeV}$) is taken to be $m_d^{\mathrm{exp}} = 4.67\,\mathrm{MeV}$.
background
The MassComparison module holds PDG 2024 experimental masses side-by-side with Recognition Science predictions. It is explicitly quarantined from the certified surface: experimental numbers are external inputs, and the RS side still depends on the anchor/yardstick system on the $\varphi$-ladder.
RS predicts a species mass as $\mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$. This definition supplies only the experimental counterpart for the down quark, quoted from Navas et al., Phys. Rev. D 110, 030001 (2024), as $4.67(48),\mathrm{MeV}$ in the MS-bar scheme at $2,\mathrm{GeV}$. Sibling constants cover $e,\mu,\tau,u,s$ and their one-sigma widths.
proof idea
No proof. The declaration is a one-line real definition binding the literal $4.67$ as the experimental central value. Uncertainty lives in the sibling m_d_exp_sigma.
why it matters
Gives the fixed experimental reference against which any RS down-quark mass prediction is residual-checked inside this verification module. Without a shared PDG anchor, machine-checked mass tables cannot report dimensionless pull or band membership. It does not itself touch the forcing chain (T0–T8), RCL, or the $\varphi$-ladder derivation; it only closes the comparison half of the ledger. Downstream residual or band lemmas in the same module would consume it as the experimental baseline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.