sin2_theta_not_half
plain-language theorem explainer
The theorem shows that the RS-derived weak mixing parameter sin²θ_W equals (3 - φ)/6 and therefore differs from the maximal-mixing value 1/2. Electroweak model builders would cite it to exclude the midpoint in the gauge-group embedding. The proof invokes the approximation lemma sin2_theta_approx, rewrites the absolute-value bound, and finishes with linear arithmetic on the resulting inequality.
Claim. $sin^2 θ_W ≠ 1/2$, where $sin^2 θ_W = (3 - φ)/6$ and $φ$ denotes the golden-ratio fixed point.
background
The module derives W and Z masses from the RS electroweak symmetry breaking, in which the Higgs VEV sits at a definite rung on the φ-ladder and the weak mixing angle emerges from the geometric embedding of the gauge groups. The explicit RS expression for the mixing parameter is supplied by the sibling definition sin2_theta_W := (3 - Constants.phi)/6. Upstream results include the anchor definitions for W and Z sectors together with the collision-free and edge-length lemmas that certify the underlying combinatorial structure.
proof idea
The term proof first obtains the absolute-value inequality from the approximation lemma sin2_theta_approx, rewrites it via the abs_lt rule, and closes the goal with linarith applied to the upper bound.
why it matters
The result rules out maximal mixing inside the RS electroweak sector, thereby preserving the predicted mass ratio m_Z = m_W / cos θ_W and the placement of the VEV near 246 GeV on the φ-ladder. It directly supports the module-level predictions m_W ≈ 80.38 GeV, m_Z ≈ 91.19 GeV and sin²θ_W ≈ 0.231. No downstream theorems are recorded, yet the inequality is a prerequisite for any further refinement of the weak-coupling constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.