m_d_exp
plain-language theorem explainer
Supplies the PDG 2024 central value for the down quark mass as the real constant 4.70 MeV. Researchers comparing Recognition Science phi-ladder predictions to data cite it as the experimental benchmark in the QuarkVerification module. The declaration is a bare numeric assignment with no lemmas or computational steps.
Claim. The experimental down-quark mass is defined as $m_d^{exp} = 4.70$ MeV (PDG 2024 MS-bar value at 2 GeV).
background
The QuarkVerification module treats experimental PDG values as quarantined constants imported for comparison, separate from certified RS derivations. Down-quark masses obey the formula $m = 2^{23} phi^{-10+r}/10^6$ MeV with rung integer r=4 for the d quark, while up-type quarks use a distinct B_pow = -1 form. This definition supplies the central PDG value 4.70 MeV as the direct numerical anchor alongside sibling constants for u, s, c, b, and t quarks.
proof idea
Direct definition that assigns the literal real number 4.70; no tactics, lemmas, or reduction steps are applied.
why it matters
Anchors the experimental side of quark mass verification against the Recognition Science phi-ladder formula derived from J-uniqueness and the eight-tick octave. It sits in the Masses domain alongside Anchor and Verification imports but remains external to the certified surface, supporting numerical checks without feeding any downstream theorems in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.