 100    True := trivial
 101
 102/-- Cornell potential value (for limit analysis). -/
 103noncomputable def cornellPotentialVal (alpha sigma r : ℝ) : ℝ :=
 104  -alpha / r + sigma * r
 105
 106/-- **THEOREM (Confinement at Long Distance)**: At large r, the potential grows linearly.
 107    V(r) - σr = -α/r → 0 as r → ∞, so V(r) ~ σr asymptotically. -/
 108theorem confinement_at_long_distance (alpha sigma : ℝ) :
 109    Filter.Tendsto (fun r => cornellPotentialVal alpha sigma r - sigma * r)
 110      Filter.atTop (nhds 0) := by
 111  unfold cornellPotentialVal
 112  simp only [add_sub_cancel_right]
 113  have h : Filter.Tendsto (fun r : ℝ => alpha / r) Filter.atTop (nhds 0) := by
 114    rw [show (0 : ℝ) = alpha * 0 from by ring]
 115    exact Filter.Tendsto.const_mul _ tendsto_inv_atTop_zero
 116  simp only [neg_div]
 117  rw [show (0 : ℝ) = -0 from by ring]
 118  exact Filter.Tendsto.neg h
 119
 120/-! ## String Picture -/
 121
 122/-- The QCD string: a flux tube connecting quark and antiquark.
 123    Energy stored in the string = σ × length. -/
 124structure QCDString where
 125  /-- Length of the string. -/
 126  length : ℝ
 127  /-- Length is positive. -/
 128  length_pos : length > 0
 129  /-- Energy stored in the string. -/
 130  energy : ℝ
 131  /-- Energy = σ × length. -/
 132  energy_eq : energy = stringTension * length
 133

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.