electroweakZeroParamScoreCardCert_holds
plain-language theorem explainer
The electroweak zero-parameter scorecard is inhabited: SM counts four free electroweak inputs while RS counts none, with α⁻¹ inside the RS band, the Weinberg-angle product fixed by φ, and four named forcing sources. Anyone auditing the RS claim that the electroweak sector is parameter-free cites this certificate. The proof is a single structure inhabitant assembling eight already-proved field lemmas.
Claim. There exists a certificate asserting: the Standard Model electroweak free-parameter count equals $4$; the RS count equals $0$; $\alpha^{-1}\in(137.030,137.039)$; $\sin^2\theta_W^{\mathrm{RS}}\cdot\cos^2\theta_W^{\mathrm{RS}}=(8-\varphi)/36$ and is positive; there are exactly four EW forcing inputs and four source theorems; and the SM-minus-RS reduction equals $4$.
background
The module formalizes the electroweak zero-parameter claim. In the Standard Model the electroweak sector is parameterized by four independent quantities $g$, $g'$, the Higgs VEV $v$, and the Higgs self-coupling $\lambda$. Recognition Science asserts that all four are forced: $\alpha^{-1}$ from the T5/T6/T7 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 $v^2=m_Z^2\sin^2\theta_W\cos^2\theta_W,\alpha^{-1}/\pi$.
The certificate structure packages eight equalities and inequalities: SM count $4$, RS count $0$, the numerical $\alpha^{-1}$ band matching the RS-native window $(137.030,137.039)$, the identity $\sin^2\theta_W\cdot\cos^2\theta_W=(8-\varphi)/36$ with positivity, finite-type cardinalities of the four forcing inputs and four source theorems, and the arithmetic reduction $4-0=4$.
Upstream lemmas already discharge each field: alpha_in_band quotes the interval bounds on $\alpha^{-1}$; rs_zero is definitional; sc_product and sc_positive fix the Weinberg product; four_forcing_inputs and four_source_theorems are decide on finite enumerations.
proof idea
Term-mode inhabitant of the certificate structure. Each field is filled by a named local lemma or rfl:
sm_paramsby definitional equality (rfl);rs_paramsbyrs_zero(rs_ew_param_count = 0);alpha_bandbyalpha_in_band(interval bounds from Numerics);sin2_cos2bysc_product;sin2_cos2_posbysc_positive(linarith on a strict lower bound);four_inputs/four_theoremsby the twodecidecardinality theorems;reductionbysm_reduction.
No new arithmetic is performed here; the proof only witnesses that the eight component results assemble into one nonempty certificate.
why it matters
This is the top-level scorecard for the electroweak zero-parameter claim in the Physics domain. It records, in one inhabitable Prop, that RS replaces the four SM electroweak free parameters by forced quantities drawn from the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick octave) together with gauge-embedding geometry and the $\varphi$-ladder mass formula.
The $\alpha^{-1}$ band field ties the certificate to the RS-native window $(137.030,137.039)$. The Weinberg product $(8-\varphi)/36$ is the geometric companion of $\sin^2\theta_W=(3-\varphi)/6$. The four-input / four-theorem cardinalities make the bookkeeping explicit: every SM parameter is matched to a named source theorem.
No downstream consumers are recorded yet; the certificate stands as the module's exportable claim that the electroweak sector is parameter-free under RS, with Lean status zero sorry and zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.