alpha_W_pos

formal source

  54  unfold alpha alphaInv alpha_seed; positivity
  55
  56/-- α_W is positive (both α and sin²θ_W are positive). -/
  57theorem alpha_W_pos : 0 < alpha_W := by
  58  unfold alpha_W
  59  exact div_pos alpha_pos_aux sin2_theta_positive
  60
  61/-- α_W > α (since sin²θ_W < 1, dividing by it increases α). -/
  62theorem alpha_W_gt_alpha : alpha < alpha_W := by
  63  unfold alpha_W
  64  rw [lt_div_iff₀ sin2_theta_positive]
  65  calc alpha * sin2_theta_W_rs
  66      < alpha * 1 := by {
  67        apply mul_lt_mul_of_pos_left _ alpha_pos_aux
  68        linarith [sin2_theta_lt_half]
  69      }
  70    _ = alpha := mul_one _
  71
  72/-- sin²θ_W > 0 (needed for division). -/
  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