sin2_theta_window
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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of sin^2 theta_W from deeper forcing-chain steps.
- Does not incorporate loop corrections or running of the angle.
- Does not address the relation to the eight-tick octave or spatial dimension D=3.
- Does not prove uniqueness of the on-shell scheme choice.
formal statement (Lean)
144theorem sin2_theta_window : 0 < sin2_theta_W ∧ sin2_theta_W < 1 := by
proof body
Term-mode proof.
145 have hs := sin2_theta_approx
146 rw [abs_lt] at hs
147 constructor
148 · linarith [hs.1]
149 · linarith [hs.2]
150
151/-- Observed weak-mixing value excludes the maximal-mixing midpoint `1/2`. -/