m_u_exp
plain-language theorem explainer
This definition supplies the PDG experimental mass of the up quark in MeV units for direct comparison against Recognition Science predictions. Researchers auditing quark mass ladders in the phi-ladder framework would reference it as the benchmark datum. The declaration is a direct numerical assignment with no derivation or computational steps.
Claim. The experimental mass of the up quark is defined as $m_{u,exp} = 2.16$ MeV.
background
The QuarkVerification module imports experimental PDG 2024 values as constants quarantined from the certified Recognition Science surface. These values benchmark the mass formula for the up-quark sector, where $m(UpQuark, r) = 2^{-1} × φ^{-5} × φ^{35} × φ^r / 10^6$ MeV simplifies to $φ^{30+r} / (2 × 10^6)$ MeV. The up quark corresponds to rung r=4 on the phi-ladder with B_pow = -1 and r0 = 35.
proof idea
This is a direct definition that assigns the numerical constant 2.16 with no lemmas or tactics applied.
why it matters
The definition anchors verification of the Recognition Science mass formula against particle data in the quark sector. It supports downstream checks of the phi-ladder predictions for generations with rungs 4, 15, and 21. The value remains outside the certified forcing chain and T5-T8 derivations, serving only as an external reference point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.