spectral_gap_pos_rung

formal source

 175  lt_of_lt_of_le one_lt_phi (phiLadder_ge_phi hn)
 176
 177/-- **Spectral gap for positive rungs**: J(φ) ≤ J(φⁿ) for n ≥ 1. -/
 178theorem spectral_gap_pos_rung {n : ℤ} (hn : 1 ≤ n) :
 179    Jcost phi ≤ Jcost (PhiLadder n) :=
 180  Jcost_mono_gt_one (phiLadder_gt_one hn) one_lt_phi (phiLadder_ge_phi hn)
 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