sin2ThetaW_RS_pos

formal source

 136theorem sin2ThetaW_RS_val : sin2ThetaW_RS = (3 - phi) / 6 := rfl
 137
 138/-- sin²θ_W^RS is positive. -/
 139theorem sin2ThetaW_RS_pos : 0 < sin2ThetaW_RS := by
 140  unfold sin2ThetaW_RS
 141  apply div_pos
 142  · linarith [phi_lt_onePointSixTwo]
 143  · norm_num
 144
 145/-- sin²θ_W^RS is less than 0.5. -/
 146theorem sin2ThetaW_RS_lt_half : sin2ThetaW_RS < 1/2 := by
 147  unfold sin2ThetaW_RS
 148  rw [div_lt_iff₀ (by norm_num : (0:ℝ) < 6)]
 149  linarith [phi_gt_onePointSixOne]
 150
 151/-- The RS prediction for sin²θ_W: ≈ (3-1.618)/6 ≈ 0.230. -/
 152theorem sin2ThetaW_RS_approx : 0.228 < sin2ThetaW_RS ∧ sin2ThetaW_RS < 0.232 := by
 153  unfold sin2ThetaW_RS
 154  constructor
 155  · rw [lt_div_iff₀ (by norm_num : (0:ℝ) < 6)]
 156    linarith [phi_lt_onePointSixTwo]
 157  · rw [div_lt_iff₀ (by norm_num : (0:ℝ) < 6)]
 158    linarith [phi_gt_onePointSixOne]
 159
 160/-! ## The Higgs Rung Assignment -/
 161
 162/-- The W-boson rung on the φ-ladder (from the mass law). -/
 163def w_rung : ℤ := 21
 164
 165/-- The Higgs rung: rung_W + Δ where Δ is derived from the Q₃ geometry.
 166
 167    The Q₃ analysis gives: the physical Higgs is the singlet (spin-0) mode
 168    of the broken SU(2). Its coupling to the Higgs mechanism is:
 169    m_H² = 2λv² where λ = sin²θ_W/(1-sin²θ_W) · m_W²/v² × (something).