BottomMSBarCert
plain-language theorem explainer
The BottomMSBarCert structure certifies that the RS rung for the bottom quark equals 21, the PDG central value is exactly 4.18 GeV and positive, and the two-loop running prediction remains positive whenever the input couplings are positive. Quark-mass phenomenologists comparing RS ladder predictions to PDG data would cite this scorecard. It is assembled directly as a structure from the module constants and positivity statements.
Claim. The structure BottomMSBarCert asserts that the RS rung satisfies $r_b=21$, the PDG mass obeys $m_b^{PDG}>0$ and equals 4.18 GeV, and the two-loop predicted mass $m_b^{pred}(α_{m_b},α_{M_Z})>0$ for all positive couplings $α_{m_b},α_{M_Z}$.
background
This module supplies a scorecard for the bottom-quark MS-bar mass inside the Recognition Science framework. The RS rung for the bottom quark (down-type, generation 3) is fixed at 21. The PDG 2024 central value is taken as the constant 4.18 GeV. The predicted mass is obtained by two-loop running of the mass at the Z scale using the function m_running with five active flavors.
proof idea
The structure is defined by direct bundling of four fields: the rung equality r_bottom = 21, the positivity and central-value statements for m_b_PDG_GeV, and the universal positivity of m_b_predicted for positive couplings. No tactics or lemmas are applied; the definition simply packages the module's constant definitions and the positivity lemma m_b_predicted_pos.
why it matters
BottomMSBarCert is instantiated by the theorem bottomMSBarCert_holds to close the scorecard for the bottom sector. It verifies the RS mass formula at rung 21 against PDG data, supporting the phi-ladder construction for down-type quarks. The module states that the scorecard carries zero axioms and zero sorrys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.