pith. machine review for the scientific record. sign in
theorem proved term proof high

m_c_predicted_pos

show as:
view Lean formalization →

The theorem establishes that the two-loop QCD running prediction for the charm quark MS-bar mass at its own scale is strictly positive when the strong coupling values at the charm scale and at the Z boson mass are positive. Researchers verifying Recognition Science structural mass predictions against experimental quark data would cite this result for sign consistency in the charm sector. The proof is a direct one-line application of the general positivity theorem for the two-loop mass running function.

claimLet $0 < alpha(m_c)$ and $0 < alpha(M_Z)$. Then the two-loop QCD running prediction for the charm quark MS-bar mass at scale $m_c$, obtained by evolving the RS-anchored value at $M_Z$ with five active flavors, satisfies $m_c^{pred}(alpha(m_c), alpha(M_Z)) > 0$.

background

The Charm Quark MS-bar Mass Scorecard module compares the Recognition Science structural prediction for the charm quark (placed at rung 15) to the PDG value $m_c(m_c) = 1.27 pm 0.02$ GeV after two-loop QCD running. The anchor mass at the $M_Z$ scale is defined as the numerical output 0.78 GeV from the gap-corrected mass formula; its positivity is established separately. The predicted mass at the charm scale is obtained by applying the two-loop mass running function to this anchor with five flavors.

proof idea

The proof unfolds the definition of the predicted mass, which applies the two-loop running engine to the anchor value, and directly invokes the upstream positivity theorem m_running_pos with the anchor mass, the two coupling values, five flavors, and the established positivity of the anchor.

why it matters in Recognition Science

This positivity result supplies the prediction component for the master certification theorem charmMSBarCert_holds that assembles rung equality, PDG positivity, and prediction positivity into the full scorecard certificate. It closes the sign check for the charm sector on the phi-ladder, consistent with the gap-corrected mass formula and the eight-tick octave structure. The module reports zero sorrys.

scope and limits

Lean usage

theorem charmMSBarCert_holds : CharmMSBarCert := { rung_eq_15 := rfl, pdg_pos := m_c_PDG_pos, pdg_central := rfl, prediction_pos := m_c_predicted_pos }

formal statement (Lean)

  80theorem m_c_predicted_pos (alpha_at_mc alpha_at_MZ : ℝ)
  81    (h_alpha_pos : 0 < alpha_at_mc) (h_alpha_0_pos : 0 < alpha_at_MZ) :
  82    0 < m_c_predicted alpha_at_mc alpha_at_MZ := by

proof body

Term-mode proof.

  83  unfold m_c_predicted
  84  exact m_running_pos m_c_at_MZ_GeV alpha_at_mc alpha_at_MZ 5
  85    m_c_at_MZ_pos h_alpha_pos h_alpha_0_pos
  86
  87/-! ## Master cert -/
  88

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.