RunningCoupling

formal source

  67
  68/-- Running coupling at scale μ. This is an abstract interface; the actual SM couplings
  69    (α_s, α, α_2) would be specializations. -/
  70structure RunningCoupling where
  71  /-- The coupling value at scale μ (in GeV). -/
  72  at_scale : ℝ → ℝ
  73  /-- The coupling is positive in the perturbative regime. -/
  74  positive_in_pert : ∀ μ, μ > 1 → at_scale μ > 0
  75  /-- Asymptotic freedom: coupling decreases at high scale (for QCD). -/
  76  asymp_free : ∀ μ₁ μ₂, μ₁ < μ₂ → μ₂ > 100 → at_scale μ₂ < at_scale μ₁
  77
  78/-- The mass anomalous dimension γ_m(μ).
  79    In general, this is a function of the scale and the fermion species.
  80    It encodes how the running mass changes with μ. -/
  81structure AnomalousDimension where
  82  /-- The anomalous dimension value for fermion f at scale μ. -/
  83  gamma : Fermion → ℝ → ℝ
  84  /-- The anomalous dimension is smooth (differentiable). -/
  85  smooth : ∀ f, Differentiable ℝ (gamma f)
  86  /-- Perturbative bound: |γ| is bounded in the perturbative regime. -/
  87  pert_bounded : ∃ B > 0, ∀ f μ, μ > 1 → |gamma f μ| < B
  88
  89/-! ## RG Transport Integral -/
  90
  91/-- The λ-normalization constant: `λ = ln(φ)`. -/
  92def lambda : ℝ := Real.log phi
  93
  94/-- λ is positive. -/
  95theorem lambda_pos : lambda > 0 := by
  96  have h : 1 < phi := one_lt_phi
  97  exact Real.log_pos h
  98
  99/-! ## Canonical one-loop beta/gamma kernels (Level-B groundwork) -/
 100