EWForcingInput
plain-language theorem explainer
Enumerates the four Recognition Science forcing-chain inputs that fix the electroweak sector: electromagnetic fine structure, Weinberg angle, Z-mass rung, and tree-level Higgs VEV. The zero-parameter scorecard cites this type to count RS free EW parameters as zero against the SM's four. It is a plain inductive enumeration with decidable equality and a finite-type instance.
Claim. An inductive type with exactly four constructors, labeling the RS-derived electroweak inputs: the electromagnetic fine-structure constant $\alpha_{\mathrm{em}}$, the Weinberg mixing angle $\theta_W$, the $Z$-boson mass rung on the $\varphi$-ladder, and the Higgs vacuum expectation value obtained from the tree-level relation.
background
In the Standard Model the electroweak sector is fixed by four independent parameters $g$, $g'$, $v$, and the Higgs self-coupling $\lambda$. Recognition Science claims 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=2\varphi^{51}/10^6$ from the $\varphi$-ladder, and $v^2=m_Z^2\sin^2\theta_W\cos^2\theta_W,\alpha^{-1}/\pi$ from the tree-level identity.
This module formalizes that zero-parameter claim as a scorecard. The inductive type names the four RS inputs so they can be counted and certified. Related constants live in Constants, mass and VEV material in the electroweak mass modules, and the $\alpha$ band in the interval numerics import.
proof idea
Definitional inductive type: four nullary constructors, no parameters, no proof obligations. The DecidableEq and Fintype deriving clauses supply equality and a finite enumeration used immediately by the cardinality theorem that the type has four elements.
why it matters
Gives the scorecard a named, finite set of forcing inputs so the RS free-parameter count can be stated as zero. Downstream, four_forcing_inputs proves the type has cardinality 4 by decide, and ElectroweakZeroParamScoreCardCert packages that count with the SM count of 4, the $\alpha^{-1}$ band $(137.030,137.039)$, and positivity of $\sin^2\theta_W\cos^2\theta_W$. Ties directly to the module claim that RS derives the EW sector from the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick) plus ladder and tree-level geometry, with no free $g,g',v,\lambda$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.