IndisputableMonolith.Masses.ElectroweakMasses
This module supplies the electroweak mass predictions and weak mixing angle in the Recognition Science framework. It states the Z boson mass lies in (91075.09, 91075.10) MeV and defines sin²θ_W = (3 − φ)/6 together with related W and Higgs quantities. Researchers deriving Standard Model parameters from the phi-ladder would cite these results. The module assembles definitions from anchor constants and phi interval bounds without internal proofs.
claimThe Z boson mass prediction satisfies $91075.09 < m_Z < 91075.10$ (MeV). The weak mixing angle is given by $\sin^2\theta_W = (3 - \phi)/6$. Related quantities include the W and Higgs mass anchors and the RS prediction z_pred.
background
The module resides in the Masses domain and imports the RS time quantum τ₀ = 1 tick from Constants, the canonical mass constants from Anchor (which centralizes parameter-free constants derived from first principles in the mass manuscripts), verification machinery from Verification, and rigorous algebraic bounds on φ = (1 + √5)/2 from PhiBounds. Sibling declarations include phi_eq_goldenRatio, m_W_exp, m_Z_exp, m_H_exp, sin2_theta_W_rs, cos2_theta_W_rs, and z_pred. The local setting is the electroweak sector of the mass ladder, where predictions are expressed via the golden-ratio fixed point and the Recognition Composition Law.
proof idea
This is a definition module, no proofs. It declares the mass predictions and mixing angle by direct reference to the imported anchor constants and the phi bounds supplied by PhiBounds.
why it matters in Recognition Science
This module feeds the definition of the weak coupling constant α_W in StandardModel.WeakCoupling, which combines α from Constants/Alpha.lean with sin²θ_W = (3 − φ)/6 supplied here. It fills the electroweak mass sector of the Recognition Science derivation chain and supplies the numerical Z-mass interval stated in the module doc-comment.
scope and limits
- Does not derive experimental mass values; they remain imported constants.
- Does not claim experimental agreement outside the stated Z-mass interval.
- Does not address strong-sector or lepton masses.
- Does not prove uniqueness of the phi-ladder assignments.
used by (1)
depends on (4)
declarations in this module (21)
-
lemma
phi_eq_goldenRatio -
def
m_W_exp -
def
m_Z_exp -
def
m_H_exp -
def
sin2_theta_W_rs -
def
cos2_theta_W_rs -
def
cos_theta_W_rs -
theorem
cos2_theta_W_rs_eq -
theorem
sin2_theta_positive -
theorem
sin2_theta_lt_half -
theorem
cos2_theta_positive -
def
z_pred -
theorem
z_pred_eq -
lemma
phi51_gt -
lemma
phi51_lt -
theorem
z_mass_bounds -
theorem
z_relative_error -
def
w_pred -
theorem
wz_ratio_eq_cos -
structure
EWCert -
theorem
ew_cert_exists