particle_content_free_params
plain-language theorem explainer
Records that the Standard Model particle content below the Z mass contributes zero free parameters to the QED running of α. Anyone citing the alpha-running scorecard or the claim that the correction ratio is fully calculable will use this constant. It is the literal natural-number 0, discharged by definitional equality.
Claim. The number of free parameters in the particle content below $M_Z$ is $0$ (the spectrum is fixed by Recognition Science).
background
The 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. RS forces $\alpha^{-1}(0)\in(137.030,137.039)$; the PDG value $\alpha^{-1}(M_Z)=127.951\pm0.009$ then implies a running ratio in $(0.933,0.935)$.
That ratio is fixed by the one-loop vacuum-polarization sum over species below $M_Z$: three charged leptons, five light quarks, and the $W$ boson, via $\Delta\alpha=\alpha/(3\pi)\sum_f N_c Q_f^2[\log(M_Z^2/m_f^2)-5/3]$. Sibling constants in the module pin $n_{\mathrm{charged,leptons}}=3$ and $n_{\mathrm{light,quarks}}=5$. The present definition simply packages the claim that this spectrum introduces no adjustable parameters.
proof idea
Pure definition: the natural number is set equal to $0$. No tactics, no lemmas. The companion theorem zero_free_params is the one-line rfl that reifies the equality.
why it matters
Closes the scorecard claim that the running correction is parameter-free. Downstream, zero_free_params is exactly particle_content_free_params = 0 by reflexivity, and AlphaRunningCorrectionScoreCardCert bundles the $\alpha^{-1}(0)$ band, the running-ratio band, and the lepton/quark counts into a single certificate. Together they discharge the module thesis: "Zero additional free parameters (particle content is RS-derived)." In the broader framework this keeps the alpha band (primer: $\alpha^{-1}$ inside $(137.030,137.039)$) free of ad-hoc SM inputs when feeding corrected VEVs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.