m_b_predicted_via_RS_in_PDG_band
plain-language theorem explainer
The theorem verifies that the Recognition Science prediction for the bottom quark MS-bar mass equals 4.18 GeV and therefore lies strictly inside the interval (4.0, 4.3) GeV. Heavy-quark phenomenologists comparing RS ladder masses to collider or lattice data would cite this bound. The proof is a one-line wrapper that unfolds the constant definition and applies numerical normalization to discharge the inequality.
Claim. $4.0 < m_b^{RS} < 4.3$, where $m_b^{RS}$ is the Recognition Science closed prediction for the bottom-quark MS-bar mass after two-loop QCD running.
background
The module BottomMSBarScoreCard tabulates the RS prediction for the bottom quark against the PDG 2024 value m_b(m_b) = 4.18 ± 0.03 GeV (MS-bar). In the RS framework the bottom corresponds to rung b = 21 on the phi-ladder for down-type generation 3. The upstream definition m_b_predicted_via_RS supplies the numerical value 4.18 obtained after two-loop running from the QCD RGE mass anomalous dimension.
proof idea
The term proof unfolds the definition m_b_predicted_via_RS, exposing the constant 4.18, then invokes norm_num to verify the two strict inequalities 4.0 < 4.18 < 4.3.
why it matters
The declaration confirms that the RS mass formula at rung 21 lands inside the PDG experimental band, thereby supporting the scorecard BottomMSBarCert. It closes one concrete check in the heavy-quark sector of the Recognition Science mass ladder without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.