phi_pow_pos

formal source

  83def PhiLadder : Set ℝ := { x | ∃ n : ℤ, x = φ^n }
  84
  85/-- φ^n is always positive for any integer n -/
  86theorem phi_pow_pos (n : ℤ) : φ^n > 0 := by
  87  exact zpow_pos phi_pos n
  88
  89/-- Adjacent rungs of the ladder have ratio φ -/
  90theorem phi_ladder_ratio (n : ℤ) : φ^(n+1) / φ^n = φ := by
  91  have h : φ ≠ 0 := ne_of_gt phi_pos
  92  have hn : φ^n ≠ 0 := zpow_ne_zero n h
  93  rw [zpow_add_one₀ h]
  94  field_simp [hn]
  95
  96/-- The ladder is closed under multiplication by φ -/
  97theorem phi_ladder_mul_closed (x : ℝ) (hx : x ∈ PhiLadder) :
  98    x * φ ∈ PhiLadder := by
  99  obtain ⟨n, rfl⟩ := hx
 100  use n + 1
 101  rw [zpow_add_one₀ (ne_of_gt phi_pos)]
 102
 103/-- The ladder is closed under division by φ -/
 104theorem phi_ladder_div_closed (x : ℝ) (hx : x ∈ PhiLadder) :
 105    x / φ ∈ PhiLadder := by
 106  obtain ⟨n, rfl⟩ := hx
 107  use n - 1
 108  rw [zpow_sub_one₀ (ne_of_gt phi_pos)]
 109  rw [div_eq_mul_inv]
 110
 111/-! ## J-cost at φ-Ladder Positions -/
 112
 113/-- J-cost formula applied to φ -/
 114theorem J_at_phi : (φ + 1/φ) / 2 - 1 = (Real.sqrt 5 - 2) / 2 :=
 115  Inequalities.J_cost_phi
 116