AlphaRunningCorrectionScoreCardCert
plain-language theorem explainer
Certificate bundle for the QED running correction of α from q²=0 to M_Z² under Recognition Science. It packages the RS α⁻¹(0) band (137.030, 137.039), the empirical ratio band (0.933, 0.935), three charged leptons, five light quarks, and zero free particle-content parameters. Anyone checking the largest radiative correction to electroweak VEVs cites this scorecard. As a structure, it has no proof body; inhabitance is discharged downstream.
Claim. A scorecard certificate consists of six facts: the RS inverse fine-structure constant at zero momentum lies in $(137.030, 137.039)$; the running ratio $\alpha^{-1}(M_Z)/\alpha^{-1}(0)$ is strictly less than $1$ and lies in $(0.933, 0.935)$; there are exactly three charged leptons and five light quarks below $M_Z$; and the particle content contributes zero free parameters.
background
The module treats the QED running of α from q²=0 to q²=M_Z² as the dominant radiative correction to electroweak mass predictions. Recognition Science forces α⁻¹(0) into (137.030, 137.039) via the forcing chain; the PDG value α⁻¹(M_Z) ≈ 127.951 then implies a correction ratio in (0.933, 0.935).
That ratio is not free: at one loop it is fixed by vacuum polarization from the particle content below M_Z (three charged leptons, five light quarks u,d,s,c,b, and the W). Locally, alpha_inv_0 is the RS constant αInv, running_ratio is α⁻¹(M_Z)/α⁻¹(0), and the lepton/quark counts and free-parameter tally are hard-coded naturals (3, 5, and 0) reflecting RS-derived content rather than fit parameters.
Upstream, the same charged-lepton count appears in the g* derivation, and VEVConsistency defines the running ratio used to correct the tree-level VEV to the physical scale.
proof idea
No proof body: this is a structure definition whose six fields are propositions (two strict open intervals for α⁻¹(0) and the running ratio, one inequality ratio < 1, and three equalities on particle counts and free parameters). Inhabitance is not shown here; the sibling theorem alphaRunningCorrectionScoreCardCert_holds builds a term by pairing the interval lemmas alpha_inv_0_gt/alpha_inv_0_lt, running_ratio_lt_one, running_ratio_gt/running_ratio_lt, and rfl on the three natural-number definitions.
why it matters
This scorecard is the typed interface for the module's claim that the largest electroweak radiative correction is RS-calculable with no extra knobs. The parent theorem alphaRunningCorrectionScoreCardCert_holds proves the structure is inhabited (Nonempty), closing the Lean status line of zero sorry and zero axiom for the scorecard.
In the broader framework it ties the forced α⁻¹(0) band from the forcing chain to the PDG M_Z anchor, and records that lepton and light-quark content below M_Z is fixed (three charged leptons, five light quarks) so the 1-loop Δα sum introduces no free parameters. Downstream VEV consistency uses the same running ratio to move the tree-level vacuum expectation value onto the physical scale; the scorecard is the audit object that those corrected-VEV claims point back to.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.