m_b_PDG_pos
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.