pith. the verified trust layer for science. sign in
module module high

IndisputableMonolith.Physics.TopMSBarScoreCard

show as:
view Lean formalization →

This module supplies RS-anchored numerical references and a certification predicate for the top quark MS-bar mass evaluated at the m_t scale, giving an approximate value of 162-163 GeV. Particle physicists matching RS mass predictions to PDG top data would cite it. The module is a definition collection that imports two-loop QCD running and pole-to-MSbar conversion formulas to produce concrete values and the TopMSBarCert predicate.

claimThe module defines the RS reference $m_t^{MS}(m_t) approx 162.5$ GeV together with the predicate TopMSBarCert asserting that the RS-predicted pole mass lies inside the PDG band after two-loop conversion.

background

The module sits inside the Heavy Quark closure track of Recognition Science. It imports the RS time quantum tau_0 = 1 tick from Constants. From MassAnomalousDimension it takes the two-loop MS-bar quark mass anomalous dimension gamma_m(a) = c_0 a + c_1 a^2. From TwoLoopAlphaS it takes the two-loop beta function for alpha_s running in the MS-bar scheme. From PoleToMSbar it takes the two-loop relation converting pole mass to MS-bar mass at the same scale with C_F = 4/3.

proof idea

This is a definition module, no proofs. It assembles imported QCD RGE formulas and PDG numerical inputs into concrete mass values (m_t_MS_at_mt_GeV, m_t_pole_predicted_via_RS) and the certification predicate topMSBarCert_holds.

why it matters in Recognition Science

The module closes the top-quark sector of the Recognition framework by supplying the MS-bar reference at m_t. It feeds the TopMSBarCert predicate that certifies consistency between the RS phi-ladder mass formula and experimental data inside the alpha band. It completes the two-loop QCD matching step required before higher-level comparisons with the eight-tick octave and D=3 spatial dimensions.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (12)