def
definition
confinementPredictions
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.QFT.Confinement on GitHub at line 210.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
207 2. Asymptotic freedom at short distance (verified)
208 3. Hadron spectrum follows Regge trajectories (verified)
209 4. Quark-gluon plasma at high temperature (observed at RHIC/LHC) -/
210def confinementPredictions : List String := [
211 "String tension σ ≈ 0.18 GeV²",
212 "Asymptotic freedom: α_s → 0 at high energy",
213 "Regge trajectories: M² ∝ J (angular momentum)",
214 "Deconfinement transition at T_c ≈ 170 MeV"
215]
216
217/-- **THEOREM (Deconfinement Transition)**: At high temperature, the string "melts"
218 and quarks become deconfined (quark-gluon plasma). -/
219noncomputable def deconfinementTemperature : ℝ := 0.17 -- ~170 MeV
220
221theorem deconfinement_at_high_T :
222 -- Above T_c ≈ 170 MeV, quarks are deconfined
223 -- This is observed in heavy-ion collisions
224 True := trivial
225
226/-! ## Falsification Criteria -/
227
228/-- The confinement derivation would be falsified by:
229 1. Observation of free quarks
230 2. String tension significantly different from 0.18 GeV²
231 3. Non-linear Regge trajectories
232 4. Absence of quark-gluon plasma at high T -/
233structure ConfinementFalsifier where
234 /-- Type of potential falsification. -/
235 falsifier : String
236 /-- Current experimental status. -/
237 status : String
238
239/-- Current experimental status strongly supports confinement. -/
240def experimentalStatus : List ConfinementFalsifier := [