Jcost_phiLadder_zero

formal source

 154  zpow_pos Constants.phi_pos n
 155
 156/-- The vacuum is at n = 0: J(φ⁰) = J(1) = 0. -/
 157theorem Jcost_phiLadder_zero : Jcost (PhiLadder 0) = 0 := by
 158  simp [PhiLadder, Jcost_unit0]
 159
 160/-- **φ-ladder reciprocal symmetry**: J(φⁿ) = J(φ⁻ⁿ). -/
 161theorem Jcost_phiLadder_symm (n : ℤ) :
 162    Jcost (PhiLadder n) = Jcost (PhiLadder (-n)) := by
 163  simp only [PhiLadder, zpow_neg]
 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