wz_ratio_equals_cos_theta
plain-language theorem explainer
The theorem shows that the ratio of predicted W and Z boson masses differs from cos of the weak mixing angle by less than 0.005. Electroweak precision studies would cite it to confirm numerical consistency between mass assignments and the Weinberg angle in the RS gauge embedding. The proof unfolds the mass and angle definitions then bounds the ratio 80.3692/91.1876 against sqrt(1-0.23122) via explicit norm_num intervals and linarith on the absolute-value split.
Claim. $|m_W / m_Z - cos θ_W| < 0.005$, where $m_W$ and $m_Z$ are the W and Z boson masses and $θ_W$ is the weak mixing angle with $sin²θ_W = 0.23122$.
background
The ElectroweakBosons module derives W and Z masses from the RS electroweak symmetry breaking picture. The vacuum expectation value sets the scale, while the weak mixing angle $θ_W$ arises from the gauge-group embedding; the module fixes $sin²θ_W = 0.23122$ numerically and defines $cos θ_W = sqrt(1 - sin²θ_W)$. The W/Z mass ratio is obtained directly from the anchored mass values $wBosonMass_GeV$ and $zBosonMass_GeV$. Upstream, cos_theta_W and sin2_theta_W supply the angle definitions, while Anchor.W and Anchor.Z provide the integer sector maps used to place the masses on the phi-ladder.
proof idea
The tactic proof first applies simp to unfold wz_mass_ratio, wBosonMass_GeV, zBosonMass_GeV, cos_theta_W and sin2_theta_W. It then introduces four norm_num lemmas that bound the ratio in (0.8813, 0.8814) and the square root in (0.8768, 0.8769). Two further lemmas establish the square-root inequalities via Real.lt_sqrt and Real.sqrt_lt_sqrt. Finally rw [abs_lt] splits the goal and linarith closes both sides of the resulting conjunction.
why it matters
The result verifies the gauge-structure identity $m_Z = m_W / cos θ_W$ inside the RS electroweak sector (module doc P-015, P-016). It supplies a concrete numerical check that the phi-ladder mass assignments remain compatible with the observed Weinberg angle. The declaration sits downstream of the mass anchors and the sin²θ_W definition; it supports later electroweak coupling approximations without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.