wBosonAbsoluteScoreCardCert_holds
plain-language theorem explainer
The W-boson absolute mass scorecard is inhabited: cos²θ_W equals (3+φ)/6 in closed form, both sin² and cos² of the RS Weinberg angle lie in fixed numerical bands, the predicted m_W/m_Z equals cos θ_W, and the derivation uses three inputs with zero free parameters. Electroweak-ladder and zero-parameter audits cite this certificate. Proof is a single structure inhabitant packing six component lemmas.
Claim. There exists a certificate that $\cos^2\theta_W^{\mathrm{RS}}=(3+\varphi)/6$, that $0.769<\cos^2\theta_W^{\mathrm{RS}}<0.771$ and $0.229<\sin^2\theta_W^{\mathrm{RS}}<0.231$, that the predicted ratio $m_W/m_Z$ equals $\cos\theta_W^{\mathrm{RS}}$, that the W-mass input set has cardinality three, and that the free-parameter count for the W mass is zero.
background
Recognition Science places the electroweak sector on the phi-ladder. The module fixes $m_Z=2\varphi^{51}/10^6$ MeV at rung 51 and takes the Weinberg angle from gauge-embedding geometry as $\sin^2\theta_W=(3-\varphi)/6$. Tree-level kinematics then give $m_W=m_Z\cos\theta_W=m_Z\sqrt{(3+\varphi)/6}$, numerically in $(79921,79922)$ MeV before radiative corrections.
The scorecard certificate packages the algebraic and numerical claims of that chain. Closed-form $\cos^2\theta_W=(3+\varphi)/6$ is the complement of the RS angle. Bands use crude interval bounds on $\varphi$ (about $1.61<\varphi<1.62$). The zero-free-parameter field follows the same definitional pattern as the SPARC, alpha-running, and gauge-coupling hierarchy scorecards.
proof idea
Term-mode inhabitant of the certificate structure. Supply cos2_theta_W_closed_form (unfold the RS angle definitions and ring) for the closed form. Pack cos2_gt and cos2_lt for the cos² band: each rewrites to the closed form and applies a $\varphi$ bound with linarith. Pack sin2_gt and sin2_lt for the sin² band. Attach wz_ratio_is_cos_theta for the mass-ratio identity, three_inputs for input cardinality, and zero_free_params (definitional reflexivity, as in sibling scorecards) for the free-parameter count.
why it matters
Top-level packing of the absolute W-mass derivation in the RS physics layer. It records that the tree-level band follows from the forcing chain with no fitted constants: $\varphi$ from T6, upstream eight-tick and dimensional structure, and the geometric fix $\sin^2\theta_W=(3-\varphi)/6$. The ~0.56% residual versus PDG 2024 is explicitly left to radiative corrections (alpha running), handled in a sibling scorecard. With no downstream dependents it is presently a leaf audit object, closing the zero-parameter plus closed-form Weinberg-angle claim for $m_W$ in the same style as the gauge-coupling and alpha-running certificates. Lean status in-module: zero sorry, zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.