phi_pow_ge_one

formal source

  51/-! ## Part 2: φ-Power Monotonicity -/
  52
  53/-- φ^n ≥ 1 for all n : ℕ. -/
  54lemma phi_pow_ge_one (n : ℕ) : 1 ≤ phi ^ n := by
  55  induction n with
  56  | zero => simp
  57  | succ k ih =>
  58    have : phi ^ (k + 1) = phi ^ k * phi := pow_succ phi k
  59    rw [this]
  60    calc 1 = 1 * 1 := by ring
  61      _ ≤ phi ^ k * phi := by
  62          exact mul_le_mul ih (le_of_lt one_lt_phi) (by norm_num) (by positivity)
  63
  64/-- φ^m < φ^n when m < n. -/
  65lemma phi_pow_strictMono {m n : ℕ} (hmn : m < n) : phi ^ m < phi ^ n := by
  66  have hphi_pos : 0 < phi := phi_pos
  67  exact pow_lt_pow_right₀ one_lt_phi hmn
  68
  69/-- **J(φ^m) < J(φ^n) FOR m < n**. -/
  70theorem Jcost_phi_pow_strictMono {m n : ℕ} (hmn : m < n) :
  71    Jcost (phi ^ m) < Jcost (phi ^ n) :=
  72  Jcost_strictMono_on_Ici_one (phi_pow_ge_one m) (phi_pow_strictMono hmn)
  73
  74/-! ## Part 3: Access Cost Properties -/
  75
  76/-- Farther access costs more. -/
  77theorem access_cost_increases_with_distance (d₁ d₂ : ℕ) (h : d₁ < d₂) :
  78    Jcost (phi ^ d₁) < Jcost (phi ^ d₂) :=
  79  Jcost_phi_pow_strictMono h
  80
  81/-- Zero distance has zero cost. -/
  82theorem access_cost_zero_at_origin : Jcost (phi ^ 0) = 0 := by
  83  simp [Jcost_unit0]
  84