WBosonAbsoluteScoreCardCert
plain-language theorem explainer
Certificate packaging the absolute W-mass scorecard: closed-form cos²θ_W = (3+φ)/6, tight numerical bands on cos² and sin² of the RS Weinberg angle, tree-level m_W/m_Z = cos θ_W, exactly three RS inputs, and zero free parameters. Anyone auditing the first-principles W prediction against PDG cites this bundle. It is a pure structure; the companion existence theorem inhabits it by assembling sibling lemmas.
Claim. A certificate asserting: $\cos^2\theta_W^{\mathrm{RS}}=(3+\varphi)/6$; $\cos^2\theta_W^{\mathrm{RS}}\in(0.769,0.771)$; $\sin^2\theta_W^{\mathrm{RS}}\in(0.229,0.231)$; the predicted ratio $m_W/m_Z$ equals $\cos\theta_W^{\mathrm{RS}}$; the W-mass input enumeration has cardinality $3$; and the free-parameter count for the W mass is $0$.
background
This module records the absolute (not ratio-only) W-boson mass chain in Recognition Science. The Z mass sits on the phi-ladder at the electroweak sector ($m_Z=2\varphi^{51}/10^6$ MeV). The RS Weinberg angle is fixed by gauge-embedding geometry: $\sin^2\theta_W^{\mathrm{RS}}=(3-\varphi)/6$, so $\cos^2\theta_W^{\mathrm{RS}}=1-\sin^2=(3+\varphi)/6$, and $\cos\theta_W^{\mathrm{RS}}=\sqrt{\cos^2}$. The tree-level W prediction is then $m_W=m_Z\cos\theta_W$.
Upstream defs supply the pieces: $\sin^2$, $\cos^2$, and $\cos$ of the RS angle; $z_\mathrm{pred}$ from the electroweak ladder mass; $w_\mathrm{pred}:=z_\mathrm{pred}\cdot\cos\theta_W^{\mathrm{RS}}$. The free-parameter counter is the constant $0$, since $\varphi$, the Z gap, and the sector index all come from the forcing chain (T5–T8 and the mass ladder). The inductive type of W-mass inputs lists exactly three constructors: phi-ladder Z mass, RS Weinberg angle, and the cosine mass relation.
proof idea
No proof body: this is a structure (certificate type) whose six fields are propositions. Inhabitation is deferred to the companion theorem, which builds a term by pairing sibling results: the closed-form identity for $\cos^2$, the four strict band inequalities on $\cos^2$ and $\sin^2$, the ratio identity $w_\mathrm{pred}/z_\mathrm{pred}=\cos\theta_W$, the Fintype cardinality of the three-input inductive type, and the definitional equality of the free-parameter counter to zero.
why it matters
The structure is the scorecard interface for the absolute W mass claim in RS. Its sole downstream consumer is the existence theorem that proves the certificate is inhabited, closing the module's "0 sorry, 0 axiom" ledger. Module narrative places the numerical target in $(79921,79922)$ MeV ($79.92$ GeV) against PDG 2024 $80.3692\pm0.0133$ GeV, residual $\sim0.56%$ ascribed to radiative running of $\alpha$, not to free fits.
Framework landmarks in play: $\varphi$ from T6 self-similarity, the phi-ladder mass formula, and the electroweak embedding that forces $\sin^2\theta_W=(3-\varphi)/6$ with no adjustable coupling. The zero-free-parameter and three-input fields make the "absolute scorecard" claim machine-checkable rather than rhetorical.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.