m_b_PDG_pos
The theorem asserts that the PDG central value for the bottom quark MS-bar mass is strictly positive. Researchers assembling Recognition Science mass scorecards for the third-generation down-type quark would cite it to satisfy the positivity clause in the BottomMSBarCert record. The proof is a one-line wrapper that unfolds the constant definition and applies numerical normalization.
claim$0 < m_b^{PDG}$ where $m_b^{PDG} := 4.18$ in GeV units.
background
The BottomMSBarScoreCard module records the experimental input for the bottom quark MS-bar mass at the scale of its own mass, drawn from PDG 2024. The sibling definition m_b_PDG_GeV hard-codes the central value 4.18 as a real number. This supplies the experimental anchor for the rung-21 entry on the phi-ladder in the Recognition Science mass formula.
proof idea
The proof is a one-line wrapper that unfolds m_b_PDG_GeV to expose the literal 4.18 and then invokes norm_num to discharge the inequality.
why it matters in Recognition Science
The result is required by the BottomMSBarCert record (downstream), which also records rung equality to 21 and positivity of the RS prediction. It closes the experimental side of the scorecard for the b-quark in the eight-tick octave framework.
scope and limits
- Does not incorporate the PDG uncertainty of 0.03 GeV.
- Does not derive the mass from the Recognition Science phi-ladder formula.
- Does not address mass running to other renormalization scales.
- Does not compare the central value against the RS prediction.
Lean usage
have h : 0 < m_b_PDG_GeV := m_b_PDG_posformal statement (Lean)
26theorem m_b_PDG_pos : 0 < m_b_PDG_GeV := by unfold m_b_PDG_GeV; norm_num
proof body
27