`vacuum`

definition

show as: view math explainer →

module: IndisputableMonolith.Unification.YangMillsMassGap
domain: Unification
line: 206 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Unification.YangMillsMassGap on GitHub at line 206.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 203  bonds : Fin 12 → ℤ
 204
 205/-- The vacuum: all bonds at rung 0. -/
 206def vacuum : GaugeBondConfig where
 207  bonds := fun _ => 0
 208
 209/-- The total J-cost of a gauge bond configuration. -/
 210def totalGaugeCost (cfg : GaugeBondConfig) : ℝ :=
 211  ∑ e ∈ (Finset.univ : Finset (Fin 12)), Jcost (PhiLadder (cfg.bonds e))
 212
 213/-- Per-bond J-costs are nonneg. -/
 214private lemma bond_cost_nonneg (cfg : GaugeBondConfig) (e : Fin 12) :
 215    0 ≤ Jcost (PhiLadder (cfg.bonds e)) :=
 216  Jcost_nonneg (phiLadder_pos (cfg.bonds e))
 217
 218/-- A single bond's cost is ≤ the total cost. -/
 219private lemma bond_le_total (cfg : GaugeBondConfig) (e : Fin 12) :
 220    Jcost (PhiLadder (cfg.bonds e)) ≤ totalGaugeCost cfg := by
 221  unfold totalGaugeCost
 222  exact Finset.single_le_sum (fun e' _ => bond_cost_nonneg cfg e') (Finset.mem_univ e)
 223
 224/-- The vacuum has zero total cost. -/
 225theorem vacuum_cost_zero : totalGaugeCost vacuum = 0 := by
 226  simp [totalGaugeCost, vacuum, Jcost_phiLadder_zero]
 227
 228/-- A configuration is non-trivial if at least one bond is not at rung 0. -/
 229def isNonTrivial (cfg : GaugeBondConfig) : Prop :=
 230  ∃ e : Fin 12, cfg.bonds e ≠ 0
 231
 232/-- **Gauge Mass Gap Theorem**: Any non-trivial gauge bond configuration
 233    has strictly positive total cost. -/
 234theorem gauge_mass_gap (cfg : GaugeBondConfig) (h : isNonTrivial cfg) :
 235    0 < totalGaugeCost cfg :=
 236  let ⟨e, he⟩ := h

papers checked against this theorem

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