m_c_predicted_via_RS_in_PDG_band
plain-language theorem explainer
The theorem shows that the Recognition Science structural prediction for the charm quark MS-bar mass at its own scale lies strictly between 1.20 and 1.34 GeV. QCD phenomenologists comparing lattice or effective-theory results to the phi-ladder mass formula would cite this bound to confirm consistency with PDG data. The proof is a one-line term reduction that unfolds the closed numerical RS value and checks the inequality by direct normalization.
Claim. The Recognition Science prediction for the charm quark mass in the MS-bar scheme satisfies $1.20 < m_c < 1.34$ in GeV units.
background
The Charm Quark MS-bar Mass Scorecard states the PDG value $m_c(m_c) = 1.27 ± 0.02$ GeV in the MS-bar scheme. Recognition Science places charm at rung c = 15 (up-type, generation 2) and obtains the structural mass via the gap-corrected formula at the anchor scale, typically $M_Z$. Two-loop running of alpha_s and the mass anomalous dimension then converts this anchor value to the MS-bar mass at the charm scale. The upstream definition supplies the closed numerical result of that two-loop engine as the constant 1.27.
proof idea
The proof is a one-line term wrapper. It unfolds the definition of the RS-predicted charm mass (the constant 1.27) and applies norm_num to verify the numerical bounds 1.20 < 1.27 < 1.34.
why it matters
This result closes the empirical scorecard check for the charm sector by placing the rung-15 RS prediction inside the PDG band after two-loop QCD evolution. It supports the mass formula yardstick * phi^(rung - 8 + gap(Z)) for heavy quarks and contributes to the validation of the eight-tick octave and phi-ladder structure. No downstream theorems depend on it in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.