WMassInput
plain-language theorem explainer
Enumerates the three Recognition-Science inputs that fix the tree-level W mass: the phi-ladder Z mass, the RS Weinberg angle, and the geometric cos-theta relation. Scorecard authors cite it to prove the free-parameter count is exactly three (hence zero fitted constants). The declaration is a finite inductive type with DecidableEq and Fintype instances.
Claim. The set of absolute inputs for the tree-level $W$ mass consists of exactly three RS-derived ingredients: (i) the $Z$ mass from the $\varphi$-ladder, (ii) the Weinberg angle fixed by RS gauge embedding, and (iii) the relation $m_W = m_Z \cos\theta_W$.
background
The W-boson absolute scorecard derives $m_W$ from first principles with no fitted parameters. The chain is: $m_Z$ sits on phi-ladder rung 51 in the electroweak sector; $\sin^2\theta_W = (3-\varphi)/6$ comes from gauge-embedding geometry; and the Standard Model identity $m_W = m_Z\cos\theta_W$ then yields the closed form $m_W = m_Z\sqrt{(3+\varphi)/6}$.
In RS-native units the numerical band is $m_W\in(79921,79922)$ MeV. The residual versus PDG 2024 is about 0.56 percent and is attributed to radiative running of $\alpha$, not to free parameters in the tree-level formula.
This inductive type simply names those three ingredients so that a Fintype cardinality proof can certify the input count.
proof idea
No proof body: the declaration is an inductive enumeration of three constructors, deriving DecidableEq and Fintype. Downstream, three_inputs obtains Fintype.card WMassInput = 3 by decide.
why it matters
The type is the formal witness that the W-mass prediction uses exactly three RS-derived ingredients and zero free parameters. It is consumed by three_inputs and by the certificate structure WBosonAbsoluteScoreCardCert, whose input_count field records Fintype.card WMassInput = 3 alongside the closed form $\cos^2\theta_W=(3+\varphi)/6$, the numerical bands, and the identity $m_W/m_Z=\cos\theta_W$.
That zero-parameter claim sits inside the broader RS forcing chain: phi is forced at T6, the electroweak ladder and gauge geometry are fixed upstream, and the scorecard closes the absolute-mass prediction for the W. The residual to PDG is left as a radiative-correction question, not a free-parameter gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.