cos2_theta_W_bounds
The theorem establishes tight numerical bounds 0.7696 < cos²θ_W < 0.7698 on the square of the cosine of the Weinberg angle inside the Recognition Science electroweak sector. Particle physicists auditing boson mass ratios against the phi-ladder would cite this result when confirming consistency with the predicted W/Z relation. The proof is a direct reduction that unfolds the definition cos²θ_W := 1 - sin²θ_W and applies linear arithmetic to the already-established bounds on sin²θ_W.
claimLet φ denote the golden ratio. Then $0.7696 < 1 - ((3 - φ)/6) < 0.7698$.
background
The electroweak sector is one of the four sectors in the Anchor.Sector inductive type (Electroweak alongside Lepton, UpQuark, DownQuark). Within this sector the Weinberg angle is fixed by the phi-ladder formula sin²θ_W = (3 − φ)/6, which follows from the self-similar fixed-point property of φ and the Recognition Composition Law. The companion theorem sin2_theta_W_bounds supplies the interval (0.2302, 0.2304) by invoking the constants phi_lt_onePointSixTwo and phi_gt_onePointFive; cos2_theta_W is then defined simply as the complement 1 - sin2_theta_W. The module imports these definitions from Masses.Anchor and Constants while remaining quarantined from experimental PDG values.
proof idea
The proof is a one-line wrapper. It unfolds the definition cos2_theta_W := 1 - sin2_theta_W, binds the hypothesis hs := sin2_theta_W_bounds, and closes both sides of the conjunction by linear arithmetic on the two endpoints of hs.
why it matters in Recognition Science
This bound is an immediate prerequisite for the downstream theorems boson_verification_cert_exists and wz_ratio_bounds, which package the electroweak verification certificate. It therefore completes the machine-checked link between the phi-ladder mass formula m(EW, r) = 2 φ^{50+r}/10^6 MeV and the observed W/Z ratio, consistent with the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain. No open scaffolding remains inside the module.
scope and limits
- Does not derive the Weinberg angle from the J-functional equation or RCL.
- Does not incorporate PDG experimental uncertainties or error propagation.
- Does not prove the kinematic relation M_Z = M_W / cos θ_W.
- Does not address radiative corrections or running of the angle.
Lean usage
rw [wz_ratio_eq_cos2]; exact cos2_theta_W_boundsformal statement (Lean)
58theorem cos2_theta_W_bounds :
59 (0.7696 : ℝ) < cos2_theta_W ∧ cos2_theta_W < (0.7698 : ℝ) := by
proof body
Term-mode proof.
60 unfold cos2_theta_W
61 have hs := sin2_theta_W_bounds
62 constructor <;> linarith [hs.1, hs.2]
63
64/-! ## Electroweak Sector Parameters -/
65