sin2thetaW_band
plain-language theorem explainer
The theorem establishes that sin²θ_W lies strictly between 0.228 and 0.232. Electroweak precision physicists would cite the bound when checking the Recognition Science prediction against collider measurements. The proof unfolds the definition sin²θ_W = (3 - φ)/6 and discharges the two-sided inequality by linear arithmetic on the supplied golden-ratio bounds.
Claim. $0.228 < (3 - φ)/6 < 0.232$ where φ is the golden ratio.
background
In the Recognition Science framework the Weinberg angle is obtained from the (3,2,1) rank decomposition of the gauge group. The module states sin²θ_W = (3 - φ)/6, which evaluates numerically to approximately 0.230. Upstream lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo supply the tight bounds 1.61 < φ < 1.62 that convert the algebraic expression into the numerical interval (0.228, 0.232).
proof idea
The proof unfolds sin2thetaW to (3 - φ)/6. It obtains the two phi bounds via the lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo. A constructor splits the conjunction; each half is discharged by linarith after rewriting the target inequality with the phi bound and the positivity of the denominator 6.
why it matters
The result supplies the band constraint required by gaugeBosonMassCert and sineSqThetaWCert. It completes the explicit numerical verification step for the Weinberg angle in §XXIII.D of the GaugeBosonSpectrum derivation. Within the framework it confirms that the RS value 0.230 lies inside 0.4 % of the PDG measurement 0.2312, linking the phi-ladder directly to an electroweak observable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.