sin2_theta_positive
plain-language theorem explainer
Physicists deriving the weak coupling α_W from the Recognition Science phi-ladder cite the positivity of sin²θ_W_rs = (3 - φ)/6. The result is invoked whenever division by this quantity must be justified. A short tactic proof unfolds the definition and reduces the inequality to the elementary bound φ < 2 via linarith.
Claim. Let φ denote the golden ratio. Then the RS Weinberg parameter satisfies $0 < (3 - φ)/6$.
background
The ElectroweakMasses module defines the RS Weinberg parameter by sin²θ_W_rs := (3 - Constants.phi)/6, where Constants.phi is identified with the golden ratio via the lemma phi_eq_goldenRatio. This expression enters the boson mass relation m_W = m_Z cos θ_W and the coupling α_W = α / sin²θ_W_rs. The module records PDG experimental masses as reference points and imports Constants, Anchor, Verification and PhiBounds.
proof idea
The tactic proof unfolds sin2_theta_W_rs to expose (3 - phi)/6. It obtains the auxiliary phi < 2 by rewriting with phi_eq_goldenRatio and applying Real.goldenRatio_lt_two. Linear arithmetic then concludes that the numerator is positive and the quotient is positive.
why it matters
The theorem is used by alpha_W_pos, alpha_W_gt_alpha, alpha_W_gt_two_alpha and sin2_pos in StandardModel.WeakCoupling. It closes the basic positivity requirement for the RS electroweak sector inside the eight-tick octave and D = 3 of the forcing chain. The parent results rely on this inequality to compare α_W with the fine-structure constant α.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.