zero_free_params
plain-language theorem explainer
The particle content entering the QED running of α from q²=0 to M_Z² contributes zero free parameters: the count is definitionally 0. Anyone assembling an AlphaRunningCorrection or SPARC-style scorecard certificate cites this to lock the no-tuning claim. The proof is reflexivity on the constant definition.
Claim. The number of free parameters associated with Standard Model particle content below $M_Z$ (charged leptons, light quarks, and the $W$ boson entering the one-loop vacuum polarization) equals $0$.
background
This module treats the QED running of the fine-structure constant from $q^2=0$ to $q^2=M_Z^2$ as the dominant radiative correction to electroweak mass predictions. Recognition Science fixes $\alpha^{-1}(0)\in(137.030,137.039)$ from the forcing chain; PDG data give $\alpha^{-1}(M_Z)\approx 127.951$, so the running ratio sits in $(0.933,0.935)$.
That ratio is not fitted. It is computed from the one-loop vacuum polarization
$\Delta\alpha=\alpha/(3\pi)\sum_f N_c Q_f^2[\log(M_Z^2/m_f^2)-5/3]$,
using the particle content below $M_Z$: three charged leptons, five light quarks, and the $W$. The definition particle_content_free_params records that this content is RS-determined and therefore contributes no adjustable knobs.
Sibling scorecards (gauge-coupling hierarchy, $W$-boson absolute mass, SPARC falsifier) use the same zero-free-parameter pattern: a natural-number constant set to 0, discharged by rfl.
proof idea
One-line reflexivity. The definition sets the free-parameter count to the natural number 0, so equality to 0 is definitional and rfl closes the goal. No lemmas are invoked.
why it matters
Closes the "zero additional free parameters" bullet of the alpha-running scorecard: particle content is RS-derived, not tuned. Downstream, alphaRunningCorrectionScoreCardCert_holds packages this with the $\alpha^{-1}(0)$ band and the running-ratio bounds into a nonempty certificate.
The same pattern feeds SPARC's global-only policy and falsifier certificate (global_only_policy, sparc_falsifier_cert), and mirrors the zero-parameter theorems on the gauge-coupling hierarchy and $W$-boson absolute scorecards. In the broader framework this supports the claim that radiative corrections to electroweak observables inherit the forcing-chain $\alpha$ band (T5–T8 landmarks, $\phi$-fixed constants) without introducing new fit parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.