zero_free_params
plain-language theorem explainer
The W-boson absolute-mass scorecard records zero RS-fitted free parameters. Anyone auditing the claim that m_W is fixed by the forcing chain alone cites this equality. The proof is reflexivity: the parameter counter is defined to be the natural number 0.
Claim. The free-parameter count for the absolute $W$ mass prediction equals $0$. All inputs ($\varphi$, the $Z$ gap, and the electroweak sector index) are taken from the Recognition Science forcing chain; none are fitted.
background
The module derives the tree-level $W$ mass from three RS ingredients only: $m_Z$ on the $\varphi$-ladder at rung 51, $\sin^2\theta_W=(3-\varphi)/6$ from gauge embedding geometry, and $m_W=m_Z\cos\theta_W=m_Z\sqrt{(3+\varphi)/6}$. The numerical band is $m_W\in(79921,79922)$ MeV, about $0.56%$ below PDG 2024, with the residual attributed to radiative running of $\alpha$.
The sibling definition free_params_w_mass is the natural-number counter of RS-fitted parameters in that chain. Its doc-comment states that every input ($\varphi$, gap$(Z)$, sector index) comes from the forcing chain, so the counter is set to $0$ by definition. Parallel counters appear on the gauge-coupling hierarchy and $\alpha$-running scorecards, and on the SPARC falsifier (per-galaxy free parameters).
proof idea
One-line term proof by rfl. The definition free_params_w_mass : ℕ := 0 makes the equality definitional; no lemmas are applied.
why it matters
This is the zero-parameter stamp on the absolute $W$ mass scorecard. Downstream, wBosonAbsoluteScoreCardCert_holds packages it into the certificate that the closed-form $\cos^2\theta_W$, the ratio $m_W/m_Z=\cos\theta_W$, and the tree-level band are free of fitted knobs. The same pattern feeds the gauge-coupling hierarchy and $\alpha$-running certificates, and the SPARC global_only_policy / sparc_falsifier_cert chain, which require every scorecard to report zero free parameters.
In the framework this is the bookkeeping side of the forcing chain (T5–T8 and the $\varphi$-ladder mass formula): once $\varphi$ and the electroweak geometry are fixed, $m_W$ is not an adjustable input. The residual versus PDG is left to radiative corrections, not to a free scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.