IndisputableMonolith.Physics.AlphaRunningCorrectionScoreCard
Scorecard module for the RS prediction of the low-energy inverse fine-structure constant α⁻¹(0) and its running ratio relative to the PDG value at the Z pole. It packages numerical bounds, the running ratio, and a free-parameter count over charged leptons and light quarks. Physicists checking the RS alpha band or electroweak consistency cite it. The content is mostly definitions and interval inequalities assembled from Constants, VEVConsistency, and AlphaBounds.
claimThe module records the RS value $\alpha^{-1}(0)$, the PDG reference $\alpha^{-1}(M_Z)$, their running ratio $r=\alpha^{-1}(0)/\alpha^{-1}(M_Z)$, interval bounds on each, and a free-parameter tally over charged leptons and light quarks that closes at zero free parameters.
background
Recognition Science targets a narrow band for the inverse fine-structure constant, with $\alpha^{-1}$ inside $(137.030, 137.039)$ in RS-native units. Running from the Z pole down to zero momentum transfer is the standard QED correction that must be scored against that band.
The module sits on three imports. Constants supplies the RS time quantum and related fixed scales. VEVConsistency shows the Higgs VEV is not independent: $v^2 = m_Z^2 \sin^2\theta_W \cos^2\theta_W ,\alpha^{-1}/\pi$. AlphaBounds supplies rigorous interval arithmetic on $\alpha^{-1}$ from the symbolic RS derivation.
Sibling definitions name $\alpha^{-1}(0)$, the PDG $\alpha^{-1}(M_Z)$, the running ratio, one-sided bounds, and particle-content counters (charged leptons, light quarks) that feed a zero-free-parameter claim.
proof idea
Definition-and-bound module rather than a single deep theorem. It introduces named constants for $\alpha^{-1}(0)$ and the PDG Z-pole value, forms their ratio, and discharges elementary interval inequalities (strict upper/lower bounds and $r<1$). Particle-content definitions count charged leptons and light quarks; those counts assemble into a free-parameter score that evaluates to zero. Heavier lifting is deferred to AlphaBounds and VEVConsistency.
why it matters in Recognition Science
Closes the low-energy end of the RS alpha story: the framework predicts a tight band for $\alpha^{-1}$, and this scorecard records both the absolute $\alpha^{-1}(0)$ figure and the running correction relative to $M_Z$. Downstream electroweak identities (VEV from $m_Z$, $\theta_W$, and $\alpha^{-1}$) need a controlled $\alpha^{-1}(0)$; the free-parameter tally supports the broader RS claim of no adjustable couplings once particle content is fixed. No further modules currently import it (used_by empty), so it functions as a leaf audit artifact for the alpha band and P5a-style consistency checks.
scope and limits
- Does not derive the symbolic RS formula for α⁻¹; that lives in AlphaBounds and upstream forcing.
- Does not prove full QED beta-function running; only scores a fixed ratio and interval bounds.
- Does not re-derive the Higgs VEV identity; it only consumes VEVConsistency.
- Does not claim experimental PDG updates; alpha_inv_mz_pdg is a fixed reference constant.
- Does not enumerate heavy quarks or bosons in the free-parameter count.
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