sm_reduction
plain-language theorem explainer
The Standard Model electroweak sector is counted as four free parameters and Recognition Science as zero, so their difference is exactly four. Anyone auditing the zero-parameter electroweak scorecard cites this equality. The proof is a one-line unfold of the two numeric definitions followed by arithmetic normalization.
Claim. If $N_{\mathrm{SM}}$ is the Standard Model electroweak free-parameter count and $N_{\mathrm{RS}}$ is the Recognition Science electroweak free-parameter count, then $N_{\mathrm{SM}} - N_{\mathrm{RS}} = 4$.
background
The module formalizes an electroweak zero-parameter scorecard. In the Standard Model the electroweak sector is treated as having four independent inputs: the gauge couplings $g$ and $g'$, the Higgs vacuum expectation value $v$, and the Higgs self-coupling $\lambda$. Recognition Science claims all four are forced rather than fitted.
Concretely, RS derives $\alpha^{-1}$ from the T5/T6/T7 forcing chain, $\sin^2\theta_W = (3-\varphi)/6$ from gauge-embedding geometry, $m_Z$ from the $\varphi$-ladder, and $v$ from the tree-level relation linking those quantities. The scorecard therefore assigns SM count 4 and RS count 0.
The two upstream definitions are pure naturals: the SM count is the constant 4 and the RS count is the constant 0. This theorem only records their difference.
proof idea
One-line wrapper. Unfold the SM electroweak parameter count (definitionally 4) and the RS electroweak parameter count (definitionally 0), then close by norm_num on the arithmetic identity $4 - 0 = 4$. No lemmas beyond definitional unfolding are required.
why it matters
The equality is a field of the electroweak zero-parameter certificate. Downstream, electroweakZeroParamScoreCardCert_holds packages it with the RS count being zero, the fine-structure constant lying in its predicted band, and the $\sin^2\theta_W\cos^2\theta_W$ product identity, witnessing that the scorecard is inhabited.
In the broader framework this is the bookkeeping step that turns the forcing-chain story (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick structure, and the geometric weak angle) into a countable claim: four SM knobs reduced to zero free RS inputs. It does not itself derive $\alpha$, $\theta_W$, $m_Z$, or $v$; it only certifies the parameter tally used by the scorecard.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.