sm_ew_param_count
plain-language theorem explainer
Fixes the Standard Model electroweak free-parameter tally at four (gauge couplings g and g', Higgs VEV v, and self-coupling λ). Scorecard and reduction lemmas cite this constant when comparing SM to the RS zero-parameter claim. The body is a bare natural-number definition.
Claim. The Standard Model electroweak sector is assigned free-parameter count $N_{\mathrm{SM}}^{\mathrm{EW}} = 4$.
background
The module Electroweak Zero-Parameter Scorecard contrasts two tallies of independent inputs in the electroweak sector. In the Standard Model those inputs are the $SU(2)_L$ and $U(1)_Y$ couplings $g$ and $g'$, the Higgs vacuum expectation value $v$, and the Higgs quartic $\lambda$.
Recognition Science instead derives the same observables from the forcing chain: $\alpha^{-1}$ from T5/T6/T7, $\sin^2\theta_W = (3-\varphi)/6$ from gauge embedding geometry, $m_Z$ from the $\varphi$-ladder, and $v$ from the tree-level relation involving $\alpha^{-1}$ and the weak mixing angles. The RS free-parameter count is therefore zero.
This definition simply records the SM side of that comparison as the natural number 4.
proof idea
No proof. The declaration is a definition that sets the constant equal to the numeral 4. Downstream lemmas unfold it and discharge equalities by norm_num.
why it matters
Anchors the SM half of the zero-parameter scorecard. The certificate structure ElectroweakZeroParamScoreCardCert requires sm_ew_param_count = 4 alongside rs_ew_param_count = 0, the $\alpha^{-1}$ band $(137.030, 137.039)$, and positivity of the RS weak-mixing product. The reduction theorem sm_reduction then states that the difference of the two counts equals 4, formalizing the claim that RS eliminates all four SM electroweak free parameters. Ties directly to the module's forcing-chain derivation of $\alpha$, $\theta_W$, $m_Z$, and $v$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.