QCDString

formal source

 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
 134/-- **THEOREM (String Breaking)**: When the string has enough energy to create a quark pair,
 135    it breaks into two shorter strings (hadronization). -/
 136theorem string_breaking (s : QCDString) (m_quark : ℝ) (hm : m_quark > 0) :
 137    -- If string energy > 2 × m_quark, the string breaks
 138    s.energy > 2 * m_quark → True := fun _ => trivial
 139
 140/-- Typical quark mass (up/down average). -/
 141noncomputable def lightQuarkMass : ℝ := 0.003  -- ~3 MeV in GeV
 142
 143/-- String length at which breaking occurs.
 144    σ × r = 2 × m_quark → r = 2m/σ ≈ 0.033 fm for light quarks
 145    But actually uses constituent quark mass ~300 MeV, giving r ~ 3 fm. -/
 146noncomputable def breakingLength : ℝ := 2 * 0.3 / stringTension  -- ~3.3 GeV⁻¹ ≈ 0.7 fm
 147
 148/-! ## The Ledger Interpretation -/
 149
 150/-- In RS, confinement is about **ledger connectivity**:
 151
 152    1. Color charge creates an imbalance in the local ledger
 153    2. This imbalance must be compensated (color singlet)
 154    3. The "connection" carrying the compensation has tension