phiLadder_pos

formal source

 150def PhiLadder (n : ℤ) : ℝ := phi ^ n
 151
 152/-- φ-ladder elements are positive. -/
 153theorem phiLadder_pos (n : ℤ) : 0 < PhiLadder n :=
 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 Δ. -/