sin2_theta_W_bounds
plain-language theorem explainer
The theorem proves that the Weinberg angle defined by (3 - φ)/6 lies strictly between 0.2302 and 0.2304. Electroweak mass modelers in Recognition Science cite it to anchor the W/Z ratio on the phi-ladder before invoking the boson verification certificate. The proof reduces directly to linear arithmetic on the two imported inequalities for φ.
Claim. $0.2302 < (3 - φ)/6 < 0.2304$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module treats electroweak boson masses via the phi-ladder formula m(EW, r) = 2 φ^{50+r} / 10^6 MeV for B_pow = 1 and r0 = 55. The Weinberg angle is introduced as the exact relation sin²θ_W = (3 - φ)/6 that links M_Z = M_W / cos θ_W. Upstream lemmas supply the numerical bounds on φ itself: phi_gt_onePointFive states (1.5 : ℝ) < φ because √5 > 2, while phi_lt_onePointSixTwo states φ < 1.62 because √5 < 2.24.
proof idea
Unfold the definition sin2_theta_W := (3 - Constants.phi)/6. Split the conjunction with constructor. Apply linarith to phi_lt_onePointSixTwo on the left and to phi_gt_onePointFive on the right.
why it matters
The bounds are packaged directly into the BosonVerificationCert constructor in boson_verification_cert_exists, which also pulls cos2_theta_W_bounds and wz_ratio_eq_cos2. They close the electroweak verification step that connects the phi-ladder rung integers to the observed W and Z masses while remaining inside the T5–T8 forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.