m_c_predicted
plain-language theorem explainer
This definition supplies the two-loop QCD-evolved charm quark MS-bar mass at its own scale from the anchor value at the Z scale. Heavy-quark phenomenologists comparing Recognition Science rung-15 predictions to PDG data would reference this computation. It is realized as a direct application of the two-loop mass evolution operator with five active flavors.
Claim. Let $m_c(m_c)$ denote the predicted MS-bar charm mass at its own scale in GeV. Then $m_c(m_c)$ equals the result of two-loop mass evolution applied to the value at the $M_Z$ scale, using the strong coupling evaluated at both the charm and $M_Z$ scales with five active flavors.
background
The Charm Quark MS-bar Mass Scorecard module evaluates the Recognition Science structural mass prediction for the charm quark, placed at rung 15 on the phi-ladder for up-type generation 2. The PDG reports the central value 1.27 GeV with uncertainty 0.02 GeV in the MS-bar scheme at its own scale. The scorecard states the RS anchor prediction, applies two-loop alpha_s running from $M_Z$ to $m_c$, applies two-loop mass running through the same interval, and compares the result to PDG. Upstream results supply the canonical arithmetic object for realization-independent counting and ledger factorization structures that calibrate the J-cost underlying discrete tier assignments.
proof idea
This definition is a one-line wrapper that invokes the two-loop mass running function at five active flavors, taking the charm mass at the Z scale together with the strong couplings at the charm and Z scales as inputs.
why it matters
This definition supplies the evolved mass value inserted into the CharmMSBarCert structure to certify agreement with the PDG band after two-loop running. It completes the mass-running step required by the scorecard in the module documentation. The underlying mass formula derives from the phi-ladder at rung 15 with gap corrections, consistent with the eight-tick octave and D=3 in the Recognition Science forcing chain from T5 through T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.