 181
 182/-- **The spectral gap theorem**: For all n ≠ 0, J(φⁿ) ≥ J(φ) > 0.
 183    Every non-vacuum φ-ladder configuration has cost at least Δ. -/
 184theorem spectral_gap (n : ℤ) (hn : n ≠ 0) :
 185    massGap ≤ Jcost (PhiLadder n) := by
 186  rw [← Jcost_phi_eq_massGap]
 187  rcases le_or_gt 1 n with h | h
 188  · exact spectral_gap_pos_rung h
 189  · have h_neg : n ≤ -1 := by omega
 190    rw [Jcost_phiLadder_symm]
 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) :

papers checked against this theorem (showing 2 of 2)

Spinning acoustic black hole still amplifies sound, but only barely
unclear · 2412.20890

"Maximum amplification ≈0.2% in solid-material ABH and rotating draining bathtub at parameters tuned to mimic extremal Kerr (Tab. IV, Fig. 7–8)"
A four-strange-quark spectrum from 2.07 to 3.12 GeV
unclear · 2507.11874

"the masses of the fully strange tetraquark states in molecular configurations with J^PC = 0++, 0−+, 0−−, 1−−, 1+−, and 1++ are investigated within the framework of QCD sum rules"