sin2_theta_approx
plain-language theorem explainer
The theorem asserts that the weak mixing angle satisfies |sin²θ_W - 0.23| < 0.01. Electroweak precision studies in Recognition Science would cite this bound when aligning the predicted Weinberg angle with collider measurements. The proof is a term-mode reduction that simplifies the constant definition and applies numerical normalization to verify the inequality.
Claim. The weak mixing angle satisfies $|sin^2 θ_W - 0.23| < 0.01$.
background
The module derives W and Z boson masses from electroweak symmetry breaking, where the Higgs VEV corresponds to a J-cost minimum and the weak mixing angle θ_W emerges from gauge-group embedding. sin²θ_W is defined locally as the constant 0.23122, chosen to match the experimental scale ≈0.231. An upstream phi-based definition (3 - phi)/6 appears in boson verification, while the spacetime interval and spin-value functions are imported but unused in this statement.
proof idea
The term proof first invokes simp only on the local definition of sin2_theta_W, then applies norm_num to discharge the absolute-value inequality by direct numerical evaluation.
why it matters
This bound anchors the electroweak predictions (m_W ≈80.38 GeV, m_Z ≈91.19 GeV, sin²θ_W ≈0.231) and is invoked directly by sin2_theta_not_half and sin2_theta_window to exclude the midpoint 1/2 and confirm the physical interval (0,1). It supplies the numerical match required by the RS gauge-embedding step within the phi-ladder and eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.