m_b_at_MZ_pos
plain-language theorem explainer
The theorem establishes positivity of the bottom-quark MS-bar mass at the Z-boson scale in GeV units. QCD modelers and Recognition Science users cite it when checking consistency of running-mass predictions on the phi-ladder for the b-quark at rung 21. The proof is a one-line wrapper that unfolds the concrete numerical definition and applies norm_num to confirm the value exceeds zero.
Claim. $0 < m_b(M_Z)$ where $m_b(M_Z)$ denotes the MS-bar bottom-quark mass evaluated at the Z-boson scale.
background
The BottomMSBarScoreCard module tabulates the bottom-quark MS-bar mass within the Recognition Science framework, taking the PDG 2024 value 4.18 ± 0.03 GeV at its own scale and assigning the b-quark to rung 21 on the phi-ladder as a down-type third-generation fermion. Upstream structures supply the J-cost from PhiForcingDerived.of, the ledger factorization from DAlembert.LedgerFactorization.of, and the emergence of SU(3) × SU(2) × U(1) gauge content with exactly three generations from SpectralEmergence.of. The local setting is a zero-sorry scorecard that anchors two-loop QCD running-mass calculations.
proof idea
The proof is a one-line wrapper. It unfolds the definition of m_b_at_MZ_GeV to expose its explicit numerical value and invokes norm_num to verify that the resulting real number is strictly positive.
why it matters
This positivity result is invoked by m_b_predicted_pos to establish that the RS-predicted bottom mass remains positive under running. It closes a basic consistency check for the third-generation down-type entry on the phi-ladder, consistent with the eight-tick octave and the J-uniqueness step of the forcing chain. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.