sin2_theta_window
plain-language theorem explainer
The theorem establishes that the squared sine of the weak mixing angle lies strictly between zero and one. Electroweak precision studies cite it to ensure the Weinberg angle yields a real cosine and a consistent W/Z mass ratio. The proof is a one-line wrapper that rewrites the absolute-value bound from the approximation lemma and splits the conjunction via linear arithmetic.
Claim. $0 < {sin}^2 theta_W < 1$, where ${sin}^2 theta_W$ denotes the on-shell weak mixing parameter.
background
The module derives W and Z boson masses from the Higgs mechanism in Recognition Science, with the vacuum expectation value at a specific phi-ladder rung. The weak mixing angle theta_W relates electromagnetic and weak couplings, and sin^2 theta_W emerges from the gauge-group embedding geometry. Two sibling definitions appear: one computes sin2_theta_W as (3 - phi)/6 and another fixes it numerically at 0.23122. The upstream sin2_theta_approx lemma states that |sin2_theta_W - 0.23| < 0.01.
proof idea
The term proof first invokes the sin2_theta_approx theorem to obtain an absolute-value inequality. It rewrites that inequality with abs_lt, then applies constructor to split the conjunction. Each conjunct is discharged by linarith using the two sides of the absolute bound.
why it matters
The result confirms that the mixing parameter remains inside the physical interval required for the mass relation m_Z = m_W / cos theta_W and for the predicted values m_W approx 80.38 GeV, m_Z approx 91.19 GeV. It supports the RS electroweak sector after the J-cost minimum and phi-ladder placement of the VEV. No downstream uses are recorded, so the lemma functions as a local sanity check rather than a parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.