pith. sign in
module module moderate

IndisputableMonolith.Physics.TopMSBarScoreCard

show as:
view Lean formalization →

This module supplies RS-anchored numerical values for the top quark MS-bar mass evaluated at the m_t scale, targeting the interval 162-163 GeV. Quark-mass phenomenologists comparing Recognition Science ladder predictions against PDG data would cite these anchors. The module assembles imported two-loop QCD running, anomalous-dimension, and pole-to-MSbar routines into concrete definitions and a certification theorem without introducing new proofs.

claimThe module defines the RS-predicted top pole mass $m_t^{ m pole}$ together with its MS-bar counterpart $m_t^{ m MS}(m_t)$ at the top-mass scale, the PDG reference values, and the proposition that the RS prediction lies inside the experimental band: $m_t^{ m MS}(m_t) \in (162,163)$ GeV.

background

The module sits inside the Recognition Science treatment of heavy-quark masses on the phi-ladder. It imports the two-loop MS-bar beta function for $\alpha_s$ (with coefficients $b_0$ and $b_1$), the two-loop quark-mass anomalous dimension $\gamma_m(\alpha_s)$ with $C_F=4/3$, and the two-loop pole-to-MSbar conversion formula that relates the PDG pole mass to the running MS-bar mass at $\mu=m_t$. Constants supplies the RS time quantum $\tau_0=1$ tick that underlies the mass-scale construction.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete numerical anchors required to test the RS mass formula against the top-quark sector. It feeds the certification step TopMSBarCert that checks consistency with PDG data and thereby closes one link in the heavy-quark closure track. The module doc-comment states its purpose as providing the RS-anchored top MS-bar mass at the m_t scale.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (12)