wz_ratio_eq_cos
plain-language theorem explainer
The declaration shows that the ratio of the predicted W and Z boson masses equals the Recognition Science value of cos(θ_W). Researchers verifying electroweak mass predictions on the phi-ladder would cite it to close the gauge relation inside the EWCert record. The proof is a direct algebraic reduction after unfolding w_pred and confirming z_pred is nonzero from the supplied mass interval.
Claim. $w_ {pred} / z_ {pred} = cos θ_W^{RS}$, where $w_ {pred}$ is defined to be $z_ {pred} × cos θ_W^{RS}$, $z_ {pred}$ is the RS mass prediction for the Z boson at rung 1, and $cos θ_W^{RS}$ is obtained from the RS formula for $sin²θ_W = (3 - φ)/6$.
background
The ElectroweakMasses module places the Z boson at rung 1 of the phi-ladder in the Electroweak sector, so that z_pred := rs_mass_MeV .Electroweak 1 lies in the interval (91075.09, 91075.10) MeV by the theorem z_mass_bounds. The W prediction is then defined by the gauge relation w_pred := z_pred * cos_theta_W_rs, where cos_theta_W_rs := sqrt(cos2_theta_W_rs) and the squared cosine follows from the RS value sin²θ_W = (3 - φ)/6 derived via the Recognition Composition Law and J-uniqueness. The module documentation states that this construction differentiates the physical assignments: Z uses rung 1 directly while W inherits the Weinberg angle factor.
proof idea
The term-mode proof unfolds the definition of w_pred to obtain the product z_pred * cos_theta_W_rs. It then introduces the auxiliary fact z_pred ≠ 0 by applying ne_of_gt to the lower bound supplied by z_mass_bounds. The final step applies mul_div_cancel_left₀ to cancel the nonzero z_pred factor, leaving the ratio equal to cos_theta_W_rs.
why it matters
The result is invoked inside ew_cert_exists to populate the wz_is_cos field of the EWCert record, thereby completing the electroweak verification certificate. It directly implements the module mechanism m_W = m_Z × cos(θ_W) with the zero-parameter RS Weinberg angle. In the larger framework it closes the gauge-boson assignment on the phi-ladder consistent with T7 eight-tick octave and D = 3, confirming that the mass predictions remain inside the narrow experimental windows without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.