sin2_theta_lt_half
plain-language theorem explainer
The RS prediction for the Weinberg angle satisfies sin²θ_W < 1/2. Particle physicists working in the Recognition Science framework cite this bound when showing that the weak coupling strength exceeds the fine-structure constant. The proof reduces the claim to the positivity of the golden ratio by unfolding the explicit formula and applying linear arithmetic.
Claim. $sin^2 θ_W = (3 - φ)/6 < 1/2$, where φ is the golden ratio supplied by the Constants structure.
background
The ElectroweakMasses module fixes the Z boson at rung 1 on the phi-ladder, giving m_Z = 2 φ^51 / 10^6 MeV, then obtains m_W via the gauge relation m_W = m_Z cos θ_W. The RS Weinberg angle is supplied by the definition sin²θ_W = (3 - φ)/6. The upstream Constants structure bundles the golden ratio together with the axiom 0 < φ.
proof idea
The term proof unfolds sin2_theta_W_rs to the expression (3 - φ)/6, invokes the lemma phi_pos to obtain 0 < φ, and concludes the inequality by linarith.
why it matters
The bound is used directly by cos2_theta_positive to prove 0 < cos²θ_W and by alpha_W_gt_alpha to establish α_W > α. It also supplies the alias sin2_lt_half in WeakCoupling. The result confirms that the RS Weinberg angle lies below 1/2, consistent with the mild mixing required for the electroweak sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.