EWSourceTheorem
plain-language theorem explainer
Finite label set for the four proved theorems that underwrite the electroweak zero-parameter claim: T5 J-cost uniqueness, T6 φ-forcing, T7 eight-tick period, and cube gauge embedding. Anyone citing the RS electroweak scorecard uses this type to name the source chain. It is a plain inductive enumeration with DecidableEq and Fintype, not a proved statement.
Claim. There is a finite type of electroweak source theorems with exactly four constructors: $J$-cost uniqueness (T5), $\varphi$-forcing (T6), the eight-tick octave (T7), and cube gauge embedding. The type carries decidable equality and a finite-type instance, so its cardinality is well-defined.
background
The electroweak zero-parameter scorecard contrasts the Standard Model count of four free EW parameters ($g$, $g'$, $v$, $\lambda$) with the RS claim that all four observables are forced. Module setup: $\alpha^{-1}$ from the T5/T6/T7 chain, $\sin^2\theta_W=(3-\varphi)/6$ from gauge embedding geometry, $m_Z$ on the $\varphi$-ladder, and $v^2$ from the tree-level relation involving $\sin^2\theta_W\cos^2\theta_W\alpha^{-1}/\pi$.
In the forcing chain, T5 fixes the cost $J(x)=(x+x^{-1})/2-1$, T6 forces $\varphi$ as the self-similar fixed point, and T7 supplies the eight-tick octave (period $2^3$). Cube gauge embedding is the geometric input for the weak mixing angle. This inductive type is the discrete tag set that records which proved theorem each forcing input traces to.
proof idea
No proof body: the declaration is an inductive type with four nullary constructors and derived DecidableEq and Fintype instances. Cardinality and equality are then discharged by decide at use sites (as in the sibling four_source_theorems).
why it matters
The scorecard’s zero-parameter claim needs an explicit, countable list of source theorems so that “four forcing inputs, four proved sources” is a machine-checkable equality rather than prose. Downstream, four_source_theorems proves Fintype.card EWSourceTheorem = 4, and ElectroweakZeroParamScoreCardCert packages that count with sm_ew_param_count = 4, rs_ew_param_count = 0, the $\alpha^{-1}$ band $(137.030,137.039)$, and positivity of $\sin^2\theta_W\cos^2\theta_W$.
Framework landmarks: T5–T7 of the unified forcing chain, plus the geometric embedding that yields $\sin^2\theta_W=(3-\varphi)/6$. The type does not itself derive $\alpha$, $\theta_W$, or $v$; it only names the four theorems the scorecard treats as the complete source list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.