w_pred
plain-language theorem explainer
The definition sets the predicted W boson mass to the product of the Z boson prediction and the RS cosine of the Weinberg angle. Electroweak mass derivations in Recognition Science cite this to enforce the gauge relation m_W = m_Z cos θ_W with zero free parameters. It is realized as a direct multiplication of the two real numbers without additional computation or lemmas.
Claim. The predicted W boson mass is $m_W = m_Z^{pred} · cos θ_W^{RS}$, where $m_Z^{pred}$ is the phi-ladder value at rung 1 in the electroweak sector and $cos θ_W^{RS}$ is the square root of the RS expression for $cos² θ_W = (3 + φ)/6$.
background
The ElectroweakMasses module places the Z boson at rung 1 of the phi-ladder in the Electroweak sector, giving the mass formula m_Z = 2 φ^51 / 10^6 MeV. The W mass is obtained from the Weinberg angle via m_W = m_Z cos θ_W, where sin² θ_W = (3 − φ)/6 supplies the RS prediction with no adjustable parameters. This definition depends on z_pred (rs_mass_MeV applied to the Electroweak sector at rung 1) and cos_theta_W_rs (the square root of the corresponding cos² term).
proof idea
This is a one-line definition that directly multiplies z_pred by cos_theta_W_rs.
why it matters
The definition supplies the W mass value required by the wz_is_cos field inside the EWCert structure and is invoked by the theorem wz_ratio_eq_cos. It implements the gauge relation stated in the module documentation, consistent with the phi-ladder mass formula and the T5–T8 forcing chain of Recognition Science. It closes the construction step that differentiates W from Z while preserving the zero-parameter character of the model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.