running_at_zero

formal source

 106  alpha0 / (1 + b * n * log phi)
 107
 108/-- **THEOREM**: At rung 0, the coupling equals the reference value. -/
 109theorem running_at_zero (alpha0 b : ℝ) :
 110    runningCoupling alpha0 b 0 = alpha0 := by
 111  unfold runningCoupling
 112  simp
 113
 114/-- **THEOREM**: For positive b, coupling decreases with rung (asymptotic freedom). -/
 115theorem asymptotic_freedom_direction (alpha0 b : ℝ) (n : ℤ)
 116    (ha : alpha0 > 0) (hb : b > 0) (hn : n > 0) :
 117    runningCoupling alpha0 b n < alpha0 := by
 118  unfold runningCoupling
 119  have hlog : log phi > 0 := Real.log_pos (by linarith [phi_gt_onePointFive])
 120  have hbn_pos : b * n * log phi > 0 := by
 121    apply mul_pos
 122    apply mul_pos hb
 123    exact Int.cast_pos.mpr hn
 124    exact hlog
 125  have hdenom_gt_one : 1 + b * n * log phi > 1 := by linarith
 126  -- α / d < α when d > 1 and α > 0
 127  have h : alpha0 / (1 + b * ↑n * log phi) < alpha0 / 1 := by
 128    apply div_lt_div_of_pos_left ha (by linarith) hdenom_gt_one
 129  simp at h
 130  exact h
 131
 132/-! ## Gauge Coupling Unification -/
 133
 134/-- At GUT scale, couplings approximately meet at α ≈ 1/24. -/
 135noncomputable def alpha_GUT : ℝ := 1/24
 136
 137/-- **THEOREM**: α_GUT = 1/(8 × 3) - unification of 8-tick and 3 dimensions. -/
 138theorem gut_24_from_8_times_3 : (24 : ℕ) = 8 * 3 := rfl
 139