charmMSBarCert_holds
plain-language theorem explainer
The declaration confirms that the Recognition Science structural prediction for the charm quark MS-bar mass at rung 15 lies inside the PDG empirical band after two-loop QCD running from the Z scale. Heavy-quark phenomenologists working inside the RS framework would cite it to close the scorecard for the second-generation up-type sector. The proof is a direct term construction that supplies the rung equality by reflexivity, the PDG positivity and central value from prior lemmas, and the prediction positivity from the mass-running result.
Claim. The RS charm MS-bar mass scorecard holds: the structural rung for charm equals 15, the PDG mass is positive and equals 1.27 GeV, and the RS-predicted mass after two-loop running is positive whenever the strong coupling at the charm scale and at the Z scale are both positive.
background
The module introduces the CharmMSBarCert structure as the closed scorecard value after two-loop running, requiring rung equality to 15 for the up-type generation-2 sector, positivity of the PDG mass, its central value of 1.27 GeV, and positivity of the predicted mass under positive couplings. The local theoretical setting is the comparison of the RS mass formula at the phi-ladder rung 15 with the empirical MS-bar value, after applying two-loop alpha_s and mass anomalous-dimension running between M_Z and the charm scale. Upstream results supply the structure definition itself together with the positivity theorems establishing 0 < m_c_PDG_GeV and the running positivity under positive couplings.
proof idea
The term proof constructs the CharmMSBarCert record directly: rung equality is supplied by reflexivity, PDG positivity by the dedicated positivity theorem, the central PDG value by reflexivity, and prediction positivity by the theorem that unfolds the two-loop mass running and applies the running-positivity lemma.
why it matters
This theorem closes the explicit scorecard for the charm quark, confirming that the RS mass formula at rung 15 together with two-loop QCD evolution reproduces the observed MS-bar mass inside the PDG band. It supports the framework claim that quark masses are fixed by the phi-ladder and sector assignments once the Recognition Composition Law and eight-tick octave are in place. No downstream uses appear in the current graph, leaving open its insertion into larger unification statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.