predicted_z_from_w
plain-language theorem explainer
The declaration supplies the predicted Z-boson mass as the W-boson mass divided by the cosine of the Weinberg angle. An electroweak phenomenologist would cite it when verifying the gauge-structure mass relation against measured values in the Recognition Science setting. The definition is a direct algebraic division of the pre-set W mass by the precomputed cosine.
Claim. The predicted Z-boson mass is $m_Z = m_W / {}$ where $m_W$ is the W-boson mass in GeV and $θ_W$ is the weak mixing angle.
background
The ElectroweakBosons module derives W and Z masses from electroweak symmetry breaking, with the Higgs VEV at approximately 246 GeV breaking SU(2)_L × U(1)_Y to U(1)_EM. The weak mixing angle θW satisfies sin²θW ≈ 0.231, and the mass relation m_Z = m_W / cos(θW) follows directly from the gauge boson mass matrix after breaking. In RS this relation is placed on the φ-ladder with the VEV at a specific rung.
proof idea
One-line definition that divides the W-boson mass value by the cosine of the Weinberg angle, using the sibling definitions of wBosonMass_GeV and cos_theta_W.
why it matters
This definition completes the electroweak mass predictions by supplying the Z mass near 91.19 GeV, consistent with the module's listed values and the gauge-structure relation after symmetry breaking. It supports tests of the RS mechanism for the weak sector and the φ-ladder placement of the electroweak scale. The result aligns with the eight-tick octave and the J-cost minimum for the VEV.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.