m_c_at_MZ_pos
plain-language theorem explainer
The Recognition Science structural prediction for the charm quark MS-bar mass at the Z-boson scale is strictly positive. QCD phenomenologists running masses between M_Z and the charm threshold would cite this result as the starting point for two-loop evolution in the scorecard. The proof is a one-line wrapper that unfolds the numerical definition and confirms positivity by normalization.
Claim. The MS-bar charm quark mass at the Z-boson scale satisfies $m_c(M_Z) > 0$ in GeV units.
background
Recognition Science places the charm quark at rung 15 on the phi-ladder for up-type generation 2. The gap-corrected mass formula combines the structural anchor with corrections drawn from the PrimitiveDistinction axioms and the phi-forcing structure. The module sets up a scorecard that states the RS prediction at the M_Z anchor, applies two-loop alpha_s and mass running down to the charm scale, and compares the resulting band to the PDG value 1.27 GeV. Upstream results establish phi-scaling for physical quantities and ledger factorization for the J-cost underlying the mass formula.
proof idea
One-line wrapper that unfolds the definition of the numerical mass value at M_Z and applies norm_num to verify the concrete floating-point quantity is positive.
why it matters
This positivity lemma is invoked directly in the proof of m_c_predicted_pos to discharge the mass-running positivity hypothesis. It closes the loop in the CharmMSBarScoreCard that compares the RS rung-15 prediction to PDG data after two-loop QCD evolution. The result supports the T6 phi fixed-point and the eight-tick octave mass ladder used throughout the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.