cornellPotential

formal source

  49
  50/-- The Cornell potential: V(r) = -α/r + σr
  51    This is the standard phenomenological form for the quark-antiquark potential. -/
  52noncomputable def cornellPotential (alpha sigma r : ℝ) (hr : r > 0) : ℝ :=
  53  -alpha / r + sigma * r
  54
  55/-- QCD coupling at short distances. -/
  56noncomputable def alphaSshort : ℝ := 0.3  -- α_s at 1 GeV scale
  57
  58/-- String tension from lattice QCD. -/
  59noncomputable def stringTension : ℝ := 0.18  -- GeV²
  60
  61/-- **THEOREM**: The potential is confining (grows with r).
  62    Proof: V(r₂) - V(r₁) = (r₂ - r₁)(α/(r₁r₂) + σ) > 0 since r₂ > r₁, α ≥ 0, σ > 0. -/
  63theorem potential_confining (alpha sigma r₁ r₂ : ℝ) (ha : alpha ≥ 0) (hs : sigma > 0)
  64    (hr₁ : r₁ > 0) (hr₂ : r₂ > r₁) :
  65    cornellPotential alpha sigma r₂ (lt_trans hr₁ hr₂)
  66    > cornellPotential alpha sigma r₁ hr₁ := by
  67  unfold cornellPotential
  68  have hr₂_pos : r₂ > 0 := lt_trans hr₁ hr₂
  69  have hr₁_ne : r₁ ≠ 0 := ne_of_gt hr₁
  70  have hr₂_ne : r₂ ≠ 0 := ne_of_gt hr₂_pos
  71  have hdiff : r₂ - r₁ > 0 := sub_pos.mpr hr₂
  72  have hr₁r₂_pos : r₁ * r₂ > 0 := mul_pos hr₁ hr₂_pos
  73  rw [show (-alpha / r₂ + sigma * r₂ > -alpha / r₁ + sigma * r₁) ↔
  74          (-alpha / r₂ + sigma * r₂ - (-alpha / r₁ + sigma * r₁) > 0) from by
  75          constructor <;> intro h <;> linarith]
  76  have h : -alpha / r₂ + sigma * r₂ - (-alpha / r₁ + sigma * r₁)
  77         = (r₂ - r₁) * (alpha / (r₁ * r₂) + sigma) := by field_simp; ring
  78  rw [h]
  79  exact mul_pos hdiff (add_pos_of_nonneg_of_pos (div_nonneg ha (le_of_lt hr₁r₂_pos)) hs)
  80
  81/-! ## J-Cost Origin of Confinement -/
  82