phiLadder_ge_phi

formal source

 164  exact Jcost_symm (zpow_pos Constants.phi_pos n)
 165
 166/-- **φⁿ ≥ φ for n ≥ 1**: the ladder climbs above φ for positive rungs. -/
 167theorem phiLadder_ge_phi {n : ℤ} (hn : 1 ≤ n) : phi ≤ PhiLadder n := by
 168  unfold PhiLadder
 169  have hge : (1 : ℝ) ≤ phi := le_of_lt one_lt_phi
 170  calc phi = phi ^ (1 : ℤ) := (zpow_one phi).symm
 171    _ ≤ phi ^ n := zpow_le_zpow_right₀ hge hn
 172
 173/-- **φⁿ > 1 for n ≥ 1**. -/
 174theorem phiLadder_gt_one {n : ℤ} (hn : 1 ≤ n) : 1 < PhiLadder n :=
 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