IndisputableMonolith.Physics.AlphaRunningCorrectionScoreCard
Scorecard module for the RS low-energy inverse fine-structure constant and its running correction toward the Z pole. It records α⁻¹(0), the PDG α⁻¹(M_Z), their ratio, interval inequalities, and a particle-content free-parameter count that closes at zero. Cite it when auditing whether the RS α band and SM charged content leave no adjustable running knobs. Structure is definitions plus elementary numeric/inequality lemmas, not a deep derivation.
claimThe module packages $ \alpha^{-1}(0) $ from Recognition Science, the PDG value $ \alpha^{-1}(M_Z) $, the running ratio $ R = \alpha^{-1}(0)/\alpha^{-1}(M_Z) $, strict bounds $ R < 1 $ and two-sided numeric windows on $ R $ and $ \alpha^{-1}(0) $, together with charged-lepton and light-quark counts that yield zero free parameters in the running correction.
background
Recognition Science fixes the inverse fine-structure constant in a narrow low-energy band (primer: $ \alpha^{-1} $ inside $ (137.030, 137.039) $). Running from $ q = 0 $ to the Z pole is the standard QED/electroweak logarithmic correction driven by charged species in the loops.
Upstream, AlphaBounds supplies rigorous interval bounds on $ \alpha^{-1} $ from the symbolic RS derivation. VEVConsistency treats $ \alpha^{-1} $ as an RS-derived input in the tree-level electroweak identity $ v^2 = m_Z^2 \sin^2\theta_W \cos^2\theta_W , \alpha^{-1}/\pi $, so the same constant must stay consistent under running. Constants anchors RS-native units ($ \tau_0 = 1 $ tick).
This module is a physics scorecard: it names the RS $ \alpha^{-1}(0) $, the PDG $ \alpha^{-1}(M_Z) $, their ratio, and the SM charged content (leptons and light quarks) used to argue the correction has no leftover free parameters.
proof idea
Definition-heavy scorecard with short inequality lemmas. Constants alpha_inv_0 and alpha_inv_mz_pdg fix the two endpoint values; running_ratio is their quotient. One-sided and two-sided comparison lemmas (alpha_inv_0_gt/lt, running_ratio_lt_one, running_ratio_gt/lt) discharge by numeric evaluation against the imported interval bounds. Particle-content definitions count charged leptons and light quarks; particle_content_free_params and zero_free_params assemble those counts into a free-parameter tally that evaluates to zero. No deep analytic running integral is proved here.
why it matters in Recognition Science
Keeps the RS $ \alpha $ prediction honest under scale change: low-energy $ \alpha^{-1}(0) $ must match the band used elsewhere (mass ladder, VEV consistency) while the Z-pole PDG anchor and SM charged content fix the running correction without new knobs. Downstream use is currently empty in the graph, so the module is a leaf audit artifact rather than a lemma feeder. It sits next to the primer $ \alpha $ band and the P5a VEV story: if the ratio or free-parameter count failed, the claim that $ \alpha^{-1} $ is fully RS-determined would not survive electroweak running. No T0–T8 forcing step is proved here; the module only scores the electromagnetic constant after those foundations.
scope and limits
- Does not derive the QED beta function or perform a loop integral.
- Does not prove the PDG $ \alpha^{-1}(M_Z) $ value; it treats it as an external anchor.
- Does not establish the RS $ \alpha^{-1}(0) $ band from first principles (defers to AlphaBounds).
- Does not address hadronic vacuum polarization beyond a light-quark count.
- Does not feed named downstream theorems in the current dependency graph.
depends on (3)
declarations in this module (14)
-
def
alpha_inv_0 -
def
alpha_inv_mz_pdg -
def
running_ratio -
theorem
alpha_inv_0_gt -
theorem
alpha_inv_0_lt -
theorem
running_ratio_lt_one -
theorem
running_ratio_gt -
theorem
running_ratio_lt -
def
n_charged_leptons -
def
n_light_quarks -
def
particle_content_free_params -
theorem
zero_free_params -
structure
AlphaRunningCorrectionScoreCardCert -
theorem
alphaRunningCorrectionScoreCardCert_holds