w_pred
w_pred defines the predicted W-boson mass as the product of the Z-boson mass prediction at rung 1 and the RS cosine of the Weinberg angle. Electroweak mass modelers cite it when checking the gauge-boson hierarchy against the phi-ladder formula. The definition is a direct algebraic product that supplies the ratio needed by the EWCert structure.
claimThe predicted W-boson mass satisfies $w = z_1^E cos theta_W^RS$, where $z_1^E$ is the Z-boson mass from the Recognition Science formula at rung 1 in the electroweak sector and $cos theta_W^RS$ is the positive square root of the RS value $(3 + phi)/6$.
background
The ElectroweakMasses module places the Z boson at rung 1 of the phi-ladder, giving the explicit mass $m_Z = 2 phi^{51}/10^6$ MeV. The W mass is obtained from the gauge relation $m_W = m_Z cos theta_W$, where the RS Weinberg angle obeys $sin^2 theta_W = (3 - phi)/6$ and therefore $cos^2 theta_W = (3 + phi)/6$. z_pred is the noncomputable real obtained by applying the rs_mass_MeV function to the Electroweak sector at rung 1. cos_theta_W_rs is defined as the positive square root of the companion cos2_theta_W_rs constant.
proof idea
The declaration is a one-line noncomputable definition that multiplies the already-defined z_pred by the precomputed cos_theta_W_rs. No lemmas or tactics are invoked; the body simply records the algebraic product required by the downstream ratio theorem.
why it matters in Recognition Science
w_pred supplies the W-mass term inside the EWCert structure, whose wz_is_cos field asserts that the W/Z ratio equals cos_theta_W_rs, and it is unfolded directly by the wz_ratio_eq_cos theorem. The definition completes the module's differentiation step: Z uses rung 1 directly while W applies the RS gauge factor derived from the phi-based Weinberg angle. It thereby anchors the electroweak predictions to the same phi-ladder used for the eight-tick octave and the alpha band.
scope and limits
- Does not derive the Weinberg angle from the J-function or the forcing chain.
- Does not evaluate the numerical W mass or compare it to PDG data.
- Does not incorporate loop corrections or running of the angle.
- Does not address the Higgs mass beyond the module's separate approximate relation.
formal statement (Lean)
121noncomputable def w_pred : ℝ := z_pred * cos_theta_W_rs
proof body
Definition body.
122
123/-- The W/Z mass ratio equals cos(θ_W) by construction. -/