cos2_theta_W_bounds
plain-language theorem explainer
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.
Claim. Let φ 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.