pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Physics.BottomMSBarScoreCard

show as:
view Lean formalization →

This module supplies RS-anchored reference values for the bottom quark MS-bar mass evaluated at the Z scale, together with PDG experimental inputs and a derived RS prediction. Physicists comparing Recognition Science mass-ladder outputs to QCD data would cite these definitions when checking the bottom rung. The module assembles imported two-loop running formulas for alpha_s and the mass anomalous dimension into a certification that the RS value lies inside the PDG band.

claimThe module defines the PDG bottom mass $m_b^PDG$ (GeV), the RS-predicted MS-bar mass $m_b(M_Z)$ obtained from the phi-ladder, and certifies that the RS value lies inside the experimental uncertainty interval at the Z scale.

background

The module sits inside the Recognition Science treatment of quark masses, where the mass formula assigns values via yardstick times phi to a power fixed by rung and gap(Z). It imports the fundamental RS time quantum tau_0 = 1 tick from Constants. The MassAnomalousDimension module supplies the two-loop MS-bar anomalous dimension gamma_m(a) = c_0 a + c_1 a^2 that governs d log m / d log mu^2. TwoLoopAlphaS supplies the two-loop beta-function running of alpha_s in the MS-bar scheme.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the bottom-mass scorecard into higher-level RS validations of the phi-ladder mass formula. It closes the heavy-quark application of the mass formula that originates in the T5 J-uniqueness and T6 phi fixed-point steps of the unified forcing chain. The certification bottomMSBarCert_holds supplies the concrete check against PDG data required by the framework.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (12)