sin2_lt_half

formal source

  73theorem sin2_pos : 0 < sin2_theta_W_rs := sin2_theta_positive
  74
  75/-- sin²θ_W < 1/2 (the weak mixing is mild). -/
  76theorem sin2_lt_half : sin2_theta_W_rs < 1/2 := sin2_theta_lt_half
  77
  78/-- α_W > 2α (since sin²θ_W < 1/2). -/
  79theorem alpha_W_gt_two_alpha : 2 * alpha < alpha_W := by
  80  unfold alpha_W
  81  rw [lt_div_iff₀ sin2_theta_positive]
  82  calc 2 * alpha * sin2_theta_W_rs
  83      < 2 * alpha * (1/2) := by {
  84        apply mul_lt_mul_of_pos_left sin2_lt_half
  85        exact mul_pos (by norm_num) alpha_pos_aux
  86      }
  87    _ = alpha := by ring
  88
  89/-! ## Part 3: Structural Certificate -/
  90
  91/-- α_W is fully RS-derived: no free parameters enter its computation.
  92    - α comes from the EMAlphaCert (44π seed + f_gap from 8-tick)
  93    - sin²θ_W = (3 − φ)/6 from gauge embedding geometry
  94    Both trace to Q₃ cube structure + golden ratio φ. -/
  95structure WeakCouplingCert where
  96  alpha_from_cube : alphaInv = alpha_seed * Real.exp (-(f_gap / alpha_seed))
  97  sin2_from_phi : sin2_theta_W_rs = (3 - Constants.phi) / 6
  98  alpha_W_def : alpha_W = alpha / sin2_theta_W_rs
  99  alpha_W_positive : 0 < alpha_W
 100  alpha_W_exceeds_alpha : alpha < alpha_W
 101
 102theorem weak_coupling_cert : WeakCouplingCert where
 103  alpha_from_cube := rfl
 104  sin2_from_phi := rfl
 105  alpha_W_def := rfl
 106  alpha_W_positive := alpha_W_pos