row_sin2_from_WZ_masses
plain-language theorem explainer
The declaration certifies that sin²θ_W computed from the PDG W and Z boson masses lies strictly between 0.22 and 0.23. Electroweak precision studies would cite this bound when assembling composite certificates for the boson mass ratio. The proof is a direct one-line reference to the upstream numerical verification theorem.
Claim. Let $m_W = 80.377$ GeV and $m_Z = 91.1876$ GeV. Define the mass ratio $r = m_W/m_Z$ and set $s = 1 - r^2$. Then $0.22 < s < 0.23$.
background
In the WZBosonRatioScoreCard module the electroweak parameter is introduced as sin²θ_W := 1 - massRatio², where massRatio is the ratio of the PDG masses m_W and m_Z. The upstream module StandardModel.WZMassRatio supplies the concrete numeric definitions of those masses together with the theorem sin2_theta_w_value that establishes the interval bounds. The module doc states that this supplies a data-interface certificate for Phase 2 (P2-WZ) rather than a first-principles derivation from the Recognition Science functional equation.
proof idea
The proof is a one-line wrapper that directly invokes sin2_theta_w_value. That upstream theorem unfolds sin2ThetaW, massRatio, m_W and m_Z, splits the conjunction, and applies norm_num to verify both strict inequalities.
why it matters
The result supplies the sin2 field of the WZBosonRatioScoreCardCert constructed in wzBosonRatioScoreCardCert_holds. It therefore participates in the partial theorem for the WZ mass ratio inside the Recognition Science framework. The RS-native formula sin²θ_W = (3-φ)/6 is proved elsewhere (Q3Representations / WeinbergAngleScoreCard); the present certificate remains a numeric data interface whose falsifier is any PDG mass update that drives the ratio outside (0.87, 0.89).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.