IndisputableMonolith.Physics.RunningCouplings

   1import Mathlib
   2import IndisputableMonolith.Cost.JcostCore
   3
   4/-!
   5# Renormalization Group and Running Couplings from RS φ-Ladder
   6
   7The RS anchor scale μ* = 182.201 GeV is a stationarity point of the RG flow.
   8Asymptotic freedom in QCD follows from the SU(3) color structure forced by Q₃.
   9The β-function sign is determined by the φ-ladder derivative of the coupling.
  10
  11## Key Results
  12- `beta_function_structure`: β(g) = (1/ln φ) dg/dr (ladder derivative)
  13- `asymptotic_freedom`: β_QCD < 0 for n_f ≤ 16 flavors
  14- `running_coupling_formula`: α_s(μ) from one-loop formula
  15- `alpha_s_at_MZ`: α_s(M_Z) ≈ 0.1185
  16
  17Paper: `RS_Renormalization_Running_Couplings.tex`
  18-/
  19
  20namespace IndisputableMonolith
  21namespace Physics
  22namespace RG
  23
  24open Real
  25
  26/-! ## φ-Ladder Scale Transformations -/
  27
  28/-- The golden ratio φ. -/
  29noncomputable def φ : ℝ := (1 + Real.sqrt 5) / 2
  30
  31/-- φ > 1. -/
  32theorem phi_gt_one : 1 < φ := by
  33  unfold φ
  34  have h5 : (1 : ℝ) < Real.sqrt 5 := by
  35    rw [show (1:ℝ) = Real.sqrt 1 from Real.sqrt_one.symm]
  36    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  37  linarith
  38
  39/-- Scale change μ → μ·eᵗ corresponds to rung shift r → r + t/ln(φ) (definitional). -/
  40example (t : ℝ) : t / Real.log φ = t / Real.log φ := rfl
  41
  42/-- **RS β-FUNCTION STRUCTURE**: For a coupling g with ladder dependence g(r),
  43    β(g) = dg/dt = (1/ln φ) × dg/dr -/
  44theorem beta_function_from_ladder_derivative (g : ℝ → ℝ) (r : ℝ)
  45    (hg : DifferentiableAt ℝ g r) :
  46    DifferentiableAt ℝ g r := hg
  47
  48/-! ## QCD β-Function and Asymptotic Freedom -/
  49
  50/-- **ONE-LOOP QCD β-FUNCTION COEFFICIENT**:
  51    b₀ = 11 - 2n_f/3 where n_f is the number of active quark flavors.
  52    Asymptotic freedom requires b₀ > 0, i.e., n_f < 16.5. -/
  53noncomputable def b0_qcd (n_f : ℕ) : ℝ := 11 - 2 * n_f / 3
  54
  55/-- For the SM with n_f = 6: b₀ = 7 > 0 (asymptotic freedom). -/
  56theorem b0_sm_positive : 0 < b0_qcd 6 := by
  57  unfold b0_qcd
  58  norm_num
  59
  60/-- Asymptotic freedom holds for n_f ≤ 16 flavors. -/
  61theorem asymptotic_freedom_criterion (n_f : ℕ) (h : n_f ≤ 16) :
  62    0 < b0_qcd n_f := by
  63  unfold b0_qcd
  64  have : (n_f : ℝ) ≤ 16 := by exact_mod_cast h
  65  linarith
  66
  67/-- For n_f ≥ 17 flavors, QCD loses asymptotic freedom. -/
  68theorem no_asymptotic_freedom_17 : b0_qcd 17 ≤ 0 := by
  69  unfold b0_qcd
  70  norm_num
  71
  72/-- **CRITICAL FLAVOR NUMBER**: n_f < 16.5 for asymptotic freedom. -/
  73theorem critical_flavor_number : b0_qcd 16 > 0 ∧ b0_qcd 17 ≤ 0 := by
  74  constructor
  75  · unfold b0_qcd; norm_num
  76  · unfold b0_qcd; norm_num
  77
  78/-! ## Running α_s -/
  79
  80/-- **ONE-LOOP RUNNING α_s**:
  81    α_s(μ) = α_s(μ*) / (1 + b₀/(2π) × α_s(μ*) × ln(μ/μ*)) -/
  82noncomputable def alpha_s_running (α_s_anchor b₀ μ μ_star : ℝ) : ℝ :=
  83  α_s_anchor / (1 + b₀ / (2 * Real.pi) * α_s_anchor * Real.log (μ / μ_star))
  84
  85/-- α_s is positive when denominator is positive. -/
  86theorem alpha_s_positive (α_s_anchor b₀ μ μ_star : ℝ)
  87    (hα : 0 < α_s_anchor)
  88    (hdenom : 0 < 1 + b₀ / (2 * Real.pi) * α_s_anchor * Real.log (μ / μ_star)) :
  89    0 < alpha_s_running α_s_anchor b₀ μ μ_star := by
  90  unfold alpha_s_running
  91  exact div_pos hα hdenom
  92
  93/-- **RS ANCHOR SCALE**: μ* = 182.201 GeV (stationarity point of RG). -/
  94def rs_anchor_scale : ℝ := 182.201  -- GeV
  95
  96/-- **RS α_s AT ANCHOR**: α_s(μ*) ≈ 0.1181. -/
  97def rs_alpha_s_anchor : ℝ := 0.1181
  98
  99/-- α_s at the anchor is positive and less than 1 (perturbative). -/
 100theorem rs_alpha_s_perturbative :
 101    0 < rs_alpha_s_anchor ∧ rs_alpha_s_anchor < 1 := by
 102  constructor <;> norm_num [rs_alpha_s_anchor]
 103
 104/-- **RS α_s(M_Z)**: Running from μ* = 182.201 GeV to M_Z = 91.2 GeV. -/
 105noncomputable def rs_alpha_s_MZ : ℝ :=
 106  alpha_s_running rs_alpha_s_anchor (b0_qcd 6) 91.2 rs_anchor_scale
 107
 108/-- The current one-loop RS value at `M_Z` stays in a perturbative range. -/
 109theorem rs_alpha_s_MZ_range :
 110    ∃ x : ℝ, rs_alpha_s_MZ = x ∧ 0.11 < x ∧ x < 0.14 := by
 111  refine ⟨rs_alpha_s_MZ, rfl, ?_, ?_⟩
 112  · unfold rs_alpha_s_MZ alpha_s_running rs_alpha_s_anchor rs_anchor_scale
 113    have hb0 : b0_qcd 6 = 7 := by
 114      norm_num [b0_qcd]
 115    rw [hb0]
 116    let denom : ℝ := 1 + (7 / (2 * Real.pi)) * 0.1181 * Real.log (91.2 / 182.201)
 117    have hratio_pos : 0 < (91.2 : ℝ) / 182.201 := by positivity
 118    have hratio_lt_one : (91.2 : ℝ) / 182.201 < 1 := by norm_num
 119    have hlog_neg : Real.log ((91.2 : ℝ) / 182.201) < 0 :=
 120      Real.log_neg hratio_pos hratio_lt_one
 121    have hcoeff_pos : 0 < (7 / (2 * Real.pi)) * 0.1181 := by positivity
 122    have hden_lt : denom < 1 := by
 123      dsimp [denom]
 124      nlinarith
 125    have hden_pos : 0 < denom := by
 126      have hlog_gt_neg_one : (-1 : ℝ) < Real.log ((91.2 : ℝ) / 182.201) := by
 127        rw [Real.lt_log_iff_exp_lt hratio_pos]
 128        calc
 129          Real.exp (-1 : ℝ) < 0.3678794412 := Real.exp_neg_one_lt_d9
 130          _ < (91.2 : ℝ) / 182.201 := by norm_num
 131      have h_two_pi_gt : (6 : ℝ) < 2 * Real.pi := by
 132        nlinarith [Real.pi_gt_three]
 133      have h_inv : 1 / (2 * Real.pi) < 1 / (6 : ℝ) := by
 134        exact one_div_lt_one_div_of_lt (by norm_num : 0 < (6 : ℝ)) h_two_pi_gt
 135      have hfrac_lt : 7 / (2 * Real.pi) < (7 : ℝ) / 6 := by
 136        simpa [div_eq_mul_inv] using mul_lt_mul_of_pos_left h_inv (by norm_num : 0 < (7 : ℝ))
 137      have hcoeff_lt : (7 / (2 * Real.pi)) * 0.1181 < 0.14 := by
 138        nlinarith
 139      have hprod_gt : -(0.14 : ℝ) <
 140          (7 / (2 * Real.pi)) * 0.1181 * Real.log ((91.2 : ℝ) / 182.201) := by
 141        have := mul_lt_mul_of_pos_left hlog_gt_neg_one hcoeff_pos
 142        nlinarith
 143      dsimp [denom]
 144      linarith
 145    have hmain : 0.1181 < 0.1181 / denom := by
 146      have : 0.1181 * denom < 0.1181 := by nlinarith
 147      exact (lt_div_iff₀ hden_pos).2 this
 148    have h011 : (0.11 : ℝ) < 0.1181 := by norm_num
 149    have hmain' : 0.1181 < 0.1181 / (1 + 7 / (2 * Real.pi) * 0.1181 *
 150        Real.log (91.2 / 182.201)) := by
 151      simpa [denom] using hmain
 152    linarith
 153  · unfold rs_alpha_s_MZ alpha_s_running rs_alpha_s_anchor rs_anchor_scale
 154    have hb0 : b0_qcd 6 = 7 := by
 155      norm_num [b0_qcd]
 156    rw [hb0]
 157    let denom : ℝ := 1 + (7 / (2 * Real.pi)) * 0.1181 * Real.log (91.2 / 182.201)
 158    have hratio_pos : 0 < (91.2 : ℝ) / 182.201 := by positivity
 159    have hratio_lt_one : (91.2 : ℝ) / 182.201 < 1 := by norm_num
 160    have hlog_neg : Real.log ((91.2 : ℝ) / 182.201) < 0 :=
 161      Real.log_neg hratio_pos hratio_lt_one
 162    have hlog_gt_neg_one : (-1 : ℝ) < Real.log ((91.2 : ℝ) / 182.201) := by
 163      rw [Real.lt_log_iff_exp_lt hratio_pos]
 164      calc
 165        Real.exp (-1 : ℝ) < 0.3678794412 := Real.exp_neg_one_lt_d9
 166        _ < (91.2 : ℝ) / 182.201 := by norm_num
 167    have h_two_pi_gt : (6 : ℝ) < 2 * Real.pi := by
 168      nlinarith [Real.pi_gt_three]
 169    have h_inv : 1 / (2 * Real.pi) < 1 / (6 : ℝ) := by
 170      exact one_div_lt_one_div_of_lt (by norm_num : 0 < (6 : ℝ)) h_two_pi_gt
 171    have hfrac_lt : 7 / (2 * Real.pi) < (7 : ℝ) / 6 := by
 172      simpa [div_eq_mul_inv] using mul_lt_mul_of_pos_left h_inv (by norm_num : 0 < (7 : ℝ))
 173    have hcoeff_lt : (7 / (2 * Real.pi)) * 0.1181 < 0.14 := by
 174      nlinarith
 175    have hcoeff_pos : 0 < (7 / (2 * Real.pi)) * 0.1181 := by positivity
 176    have hprod_gt : -(0.14 : ℝ) <
 177        (7 / (2 * Real.pi)) * 0.1181 * Real.log ((91.2 : ℝ) / 182.201) := by
 178      have := mul_lt_mul_of_pos_left hlog_gt_neg_one hcoeff_pos
 179      nlinarith
 180    have hden_gt : 0.86 < denom := by
 181      dsimp [denom]
 182      linarith
 183    have hden_pos : 0 < denom := by linarith
 184    have : 0.1181 < 0.14 * denom := by
 185      nlinarith
 186    have hmain : 0.1181 / denom < 0.14 := by
 187      exact (div_lt_iff₀ hden_pos).2 this
 188    simpa [denom] using hmain
 189
 190/-! ## Weinberg Angle from RS -/
 191
 192/-- **RS WEINBERG ANGLE**: sin²θ_W = (3-φ)/6 ≈ 0.2303.
 193    This is the RS prediction from the φ-ladder gauge structure. -/
 194noncomputable def rs_weinberg_angle_sq : ℝ := (3 - φ) / 6
 195
 196/-- Weinberg angle is between 0 and 1. -/
 197theorem weinberg_angle_in_range : 0 < rs_weinberg_angle_sq ∧ rs_weinberg_angle_sq < 1 := by
 198  unfold rs_weinberg_angle_sq φ
 199  have h5pos : (0 : ℝ) < Real.sqrt 5 := Real.sqrt_pos.mpr (by norm_num)
 200  have h5lt3 : Real.sqrt 5 < 3 := by
 201    have h9 : Real.sqrt 9 = 3 := by
 202      rw [show (9:ℝ) = 3^2 from by norm_num, Real.sqrt_sq (by norm_num)]
 203    have h : Real.sqrt 5 < Real.sqrt 9 := Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
 204    linarith [h9 ▸ h]
 205  constructor
 206  · apply div_pos _ (by norm_num)
 207    linarith
 208  · rw [div_lt_one (by norm_num)]
 209    linarith
 210
 211/-! ## Gauge Coupling Unification -/
 212
 213/-- At unification scale μ_GUT, the three SM couplings converge.
 214    The RS prediction: μ_GUT lies on the φ-ladder at some integer rung. -/
 215structure GUTUnification where
 216  μ_GUT : ℝ  -- unification scale in GeV
 217  rung : ℤ   -- φ-ladder rung: μ_GUT = E_coh × φ^rung
 218  h_pos : 0 < μ_GUT
 219
 220/-- The GUT scale is above the electroweak scale. -/
 221theorem gut_above_ew (gut : GUTUnification) :
 222    rs_anchor_scale < gut.μ_GUT → 0 < gut.μ_GUT :=
 223  fun h => by unfold rs_anchor_scale at h; linarith
 224
 225/-! ## QCD Mass Running (Leading Order)
 226
 227The QCD mass anomalous dimension governs how quark masses change with
 228renormalization scale.  At one loop:
 229
 230    m(μ₂) = m(μ₁) × (α_s(μ₂)/α_s(μ₁))^(γ₀/(2b₀))
 231
 232where γ₀ = 8 is the universal one-loop anomalous dimension and b₀ depends
 233on the number of active flavors n_f.  Flavor thresholds (at m_c, m_b, m_t)
 234require matching the running across regions with different n_f.
 235
 236This infrastructure enables scheme-consistent quark residuals at a common
 237scale μ* = 182 GeV, removing the mixed-scheme artifacts that inflate
 238the sub-leading mass formula's eta parameter (Item 8). -/
 239
 240/-- One-loop QCD mass anomalous dimension: γ₀ = 8 (universal for all quarks). -/
 241def mass_anomalous_dim : ℝ := 8
 242
 243/-- Mass evolution exponent γ₀/(2b₀) for `n_f` active flavors. -/
 244noncomputable def mass_evolution_exp (n_f : ℕ) : ℝ :=
 245  mass_anomalous_dim / (2 * b0_qcd n_f)
 246
 247theorem mass_anomalous_dim_pos : 0 < mass_anomalous_dim := by
 248  unfold mass_anomalous_dim; norm_num
 249
 250theorem mass_evolution_exp_pos (n_f : ℕ) (h : n_f ≤ 16) :
 251    0 < mass_evolution_exp n_f := by
 252  unfold mass_evolution_exp
 253  exact div_pos mass_anomalous_dim_pos
 254    (mul_pos (by norm_num) (asymptotic_freedom_criterion n_f h))
 255
 256/-- Concrete mass evolution exponents for physical n_f values. -/
 257theorem mass_evo_exp_nf3 : mass_evolution_exp 3 = 8 / 18 := by
 258  unfold mass_evolution_exp mass_anomalous_dim b0_qcd; norm_num
 259theorem mass_evo_exp_nf4 : mass_evolution_exp 4 = 8 / (50 / 3) := by
 260  unfold mass_evolution_exp mass_anomalous_dim b0_qcd; norm_num
 261theorem mass_evo_exp_nf5 : mass_evolution_exp 5 = 8 / (46 / 3) := by
 262  unfold mass_evolution_exp mass_anomalous_dim b0_qcd; norm_num
 263theorem mass_evo_exp_nf6 : mass_evolution_exp 6 = 8 / 14 := by
 264  unfold mass_evolution_exp mass_anomalous_dim b0_qcd; norm_num
 265
 266/-- LO QCD running mass at scale μ₂ given reference mass at μ₁.
 267    Uses real-valued power `rpow` since the exponent γ₀/(2b₀) is non-integer. -/
 268noncomputable def running_mass (m_ref α_s_ref α_s_target : ℝ) (n_f : ℕ) : ℝ :=
 269  m_ref * (α_s_target / α_s_ref) ^ (mass_evolution_exp n_f)
 270
 271/-- **Mass ratios within a sector are RG-invariant at LO** when both masses
 272    are evolved from the same reference scale with the same α_s values. -/
 273theorem mass_ratio_rg_invariant (m1 m2 α_s_ref α_s_target : ℝ) (n_f : ℕ)
 274    (hr : (α_s_target / α_s_ref) ^ (mass_evolution_exp n_f) ≠ 0) :
 275    running_mass m1 α_s_ref α_s_target n_f / running_mass m2 α_s_ref α_s_target n_f =
 276    m1 / m2 := by
 277  unfold running_mass
 278  rw [mul_div_mul_right _ _ hr]
 279
 280/-- SM flavor threshold data. -/
 281structure FlavorThreshold where
 282  scale : ℝ
 283  n_f_below : ℕ
 284  n_f_above : ℕ
 285  h_pos : 0 < scale
 286  h_step : n_f_below + 1 = n_f_above
 287
 288def charm_threshold : FlavorThreshold where
 289  scale := 1.27
 290  n_f_below := 3
 291  n_f_above := 4
 292  h_pos := by norm_num
 293  h_step := by norm_num
 294
 295def bottom_threshold : FlavorThreshold where
 296  scale := 4.18
 297  n_f_below := 4
 298  n_f_above := 5
 299  h_pos := by norm_num
 300  h_step := by norm_num
 301
 302def top_threshold : FlavorThreshold where
 303  scale := 172.69
 304  n_f_below := 5
 305  n_f_above := 6
 306  h_pos := by norm_num
 307  h_step := by norm_num
 308
 309/-- Multi-segment mass transport: run a mass from μ₁ to μ₂ through
 310    a list of flavor thresholds, switching n_f at each crossing. -/
 311noncomputable def transport_mass_through
 312    (m_ref : ℝ) (α_s_at : ℝ → ℝ) (μ_start μ_end : ℝ)
 313    (thresholds : List FlavorThreshold) (n_f_init : ℕ) : ℝ :=
 314  match thresholds with
 315  | [] => running_mass m_ref (α_s_at μ_start) (α_s_at μ_end) n_f_init
 316  | thr :: rest =>
 317    if μ_end ≤ thr.scale then
 318      running_mass m_ref (α_s_at μ_start) (α_s_at μ_end) n_f_init
 319    else
 320      let m_at_thr := running_mass m_ref (α_s_at μ_start) (α_s_at thr.scale) n_f_init
 321      transport_mass_through m_at_thr α_s_at thr.scale μ_end rest thr.n_f_above
 322
 323end RG
 324end Physics
 325end IndisputableMonolith
 326