`spectral_gap_strict`

proved

show as: view math explainer →

module: IndisputableMonolith.Unification.YangMillsMassGap
domain: Unification
line: 194 · 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 194.

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

 191    apply spectral_gap_pos_rung; omega
 192
 193/-- **Strict spectral gap**: Every non-vacuum configuration has strictly positive cost. -/
 194theorem spectral_gap_strict (n : ℤ) (hn : n ≠ 0) :
 195    0 < Jcost (PhiLadder n) :=
 196  lt_of_lt_of_le massGap_pos (spectral_gap n hn)
 197
 198/-! ## §5  Gauge Field Excitations Carry Positive Cost -/
 199
 200/-- A gauge bond configuration: each of Q₃'s 12 edges carries a bond
 201    multiplier rung index. The vacuum has all multipliers at rung 0 = φ⁰ = 1. -/
 202structure GaugeBondConfig where
 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. -/

papers checked against this theorem

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