potential_confining
The Cornell potential is strictly increasing for positive separations when the Coulomb coefficient is non-negative and the string tension is positive. QCD modelers would cite this to confirm linear growth of the confining term from J-cost scaling. The proof reduces the inequality to a factored positive expression via field simplification and ring algebra after unfolding the potential definition.
claimLet $V(r) = -alpha/r + sigma r$. Then for $alpha >= 0$, $sigma > 0$, $r_1 > 0$ and $r_2 > r_1$, it holds that $V(r_2) > V(r_1)$.
background
In Recognition Science the Cornell potential models the effective interaction between color charges as $V(r) = -alpha/r + sigma r$, with the linear term arising from J-cost distance scaling. The J-cost is the derived cost function of a multiplicative recognizer comparator, as defined in MultiplicativeRecognizerL4.cost, which quantifies ledger imbalance for separated charges. Module SM-007 derives QCD confinement by showing this potential grows with distance, producing the constant string tension that favors hadronization over isolation.
proof idea
The tactic proof unfolds cornellPotential, introduces positivity facts for r2 and the radius difference via lt_trans and sub_pos, then rewrites the target inequality equivalently as positivity of the difference. Field_simp followed by ring factors the difference as (r2 - r1) times (alpha/(r1 r2) + sigma). The final exact step applies mul_pos to the two manifestly positive factors.
why it matters in Recognition Science
This result establishes the confining (linearly growing) character of the potential, directly supporting the long-distance behavior in the J-cost model of confinement. It supplies the algebraic step needed for confinement_at_long_distance and string_breaking within the module. The theorem connects to the Recognition Composition Law by making explicit the distance-dependent cost that enforces the eight-tick octave scaling into D=3 spatial dimensions and the observed alpha band.
scope and limits
- Does not assign a numerical value to the string tension sigma.
- Does not derive the short-distance Coulomb or asymptotic-freedom regime.
- Does not incorporate quantum loop corrections or running of alpha.
- Does not extend to negative alpha or zero string tension.
formal statement (Lean)
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
proof body
Tactic-mode proof.
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
83/-- In RS, the confining potential comes from J-cost of maintaining color separation:
84
85 1. Color charge is a "ledger imbalance"
86 2. Separating charges stretches the ledger connection
87 3. The cost of stretching grows with distance
88 4. This creates the linear σr term -/