four_forcing_inputs
plain-language theorem explainer
The electroweak forcing-input type has exactly four inhabitants: electromagnetic coupling, Weinberg angle, Z mass rung, and tree-level VEV. Anyone citing the RS zero-parameter electroweak scorecard needs this cardinality fact. The proof is a one-line finite-type decision on the inductive constructors.
Claim. The finite type of Recognition Science electroweak forcing inputs has cardinality $4$. Those four inputs are the electromagnetic fine-structure input, the Weinberg angle, the $Z$-boson mass rung on the $\phi$-ladder, and the vacuum expectation value fixed by the tree-level relation.
background
The module formalizes the electroweak zero-parameter scorecard. In the Standard Model the electroweak sector is counted as four free parameters ($g$, $g'$, $v$, and the Higgs self-coupling $\lambda$). Recognition Science claims all four are forced, so the RS free-parameter count is zero.
The inductive type of forcing inputs enumerates the four RS sources named in the module doc: $\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 relation. The type derives Fintype, so its cardinality is a decidable natural-number equality.
proof idea
Term-mode proof by decide. Because EWForcingInput derives Fintype and DecidableEq, Lean enumerates the four constructors and closes Fintype.card _ = 4 by computation. No lemmas beyond the derived instances are required.
why it matters
This cardinality fact is the bookkeeping step that lets the scorecard assert RS has zero free electroweak parameters against SM's four. It is consumed by electroweakZeroParamScoreCardCert_holds, which packages the certificate (SM param count, RS param count zero, $\alpha$ in band, and the $\sin^2\cos^2$ product identity).
In the broader framework it records that the electroweak sector is pinned by the forcing chain landmarks already listed in the module: T5 J-uniqueness and T6 $\varphi$, the eight-tick structure behind the $\alpha$ formula, the $\varphi$-ladder mass rung for $m_Z$, and the geometric Weinberg angle. Without a proved four-count, the zero-parameter claim would be informal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.