alphaRunningCorrectionScoreCardCert_holds
plain-language theorem explainer
Packages the full alpha-running scorecard into a single inhabited certificate: RS-native α⁻¹(0) sits in (137.030, 137.039), the PDG ratio α⁻¹(M_Z)/α⁻¹(0) lies in (0.933, 0.935) and is strictly less than 1, and the particle content is fixed at 3 charged leptons and 5 light quarks with zero free parameters. Anyone citing the radiative correction to electroweak VEVs from RS α(0) needs this bundle. Proof is a pure structure inhabitant assembling six already-proved component lemmas.
Claim. There exists a certificate asserting: $137.030 < \alpha^{-1}(0) < 137.039$; the running ratio $r = \alpha^{-1}(M_Z)/\alpha^{-1}(0)$ satisfies $r < 1$ and $0.933 < r < 0.935$; the charged-lepton count is $3$; the light-quark count is $5$; and the particle-content free-parameter count is $0$.
background
QED vacuum polarization runs the fine-structure constant from $q^2=0$ to $q^2=M_Z^2$. That running is the dominant radiative correction feeding electroweak mass predictions. Recognition Science forces $\alpha^{-1}(0)$ into the open interval $(137.030, 137.039)$ via the forcing chain (the alpha band of the primer). PDG quotes $\alpha^{-1}(M_Z)=127.951\pm 0.009$, so the ratio $r=\alpha^{-1}(M_Z)/\alpha^{-1}(0)$ must land in $(0.933,0.935)$.
The ratio is not a free fit parameter. At one loop it is fixed by the charged spectrum below $M_Z$: three charged leptons, five light quarks, and the $W$ boson, through $\Delta\alpha=\alpha/(3\pi)\sum_f N_c Q_f^2[\log(M_Z^2/m_f^2)-5/3]$. The module therefore records both the numerical band on $r$ and the discrete particle counts, together with a zero-free-parameter claim.
Upstream lemmas already discharge each numeric inequality: alpha_inv_0_gt / alpha_inv_0_lt wrap the Numerics interval bounds on $\alpha^{-1}(0)$; running_ratio_gt / running_ratio_lt rearrange those bounds against the fixed PDG value $127.951$; running_ratio_lt_one records screening ($r<1$).
proof idea
Term-mode inhabitant of the certificate structure. Each field is filled by a named sibling lemma:
alpha_0_bandis the pair⟨alpha_inv_0_gt, alpha_inv_0_lt⟩(Numerics interval on $\alpha^{-1}(0)$).ratio_lt_oneisrunning_ratio_lt_one.ratio_bandis the pair⟨running_ratio_gt, running_ratio_lt⟩(division inequalities against $127.951$).leptonsandquarksare definitional equalities (rfl) fixing counts $3$ and $5$.zero_paramsiszero_free_params(particle-content free-parameter count is definitionally $0$).
No new arithmetic is performed; the certificate is pure packaging.
why it matters
Closes the module's scorecard: every claim listed in the module doc (correction-ratio band, RS-native $\alpha(0)$ band, fixed particle content, zero extra free parameters) is now available as one Nonempty certificate. Downstream electroweak or VEV-consistency arguments can demand this certificate rather than re-proving the six component facts.
Framework landmarks touched: the RS alpha band $(137.030,137.039)$ forced by the chain, and the claim that the largest radiative correction to mass predictions introduces no new free parameters once the RS-derived spectrum (3 charged leptons, 5 light quarks) is fixed. The module doc also states that the corrected VEV from RS-native $\alpha(0)$ falls in the PDG band; this certificate is the numeric gate for that claim.
No downstream users are recorded yet (used_by_count = 0), so the immediate consumer is expected to be a VEV-consistency or electroweak mass theorem that imports this scorecard.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.