phi_pow_strictMono

formal source

  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
  85/-- Nonzero distance has positive cost. -/
  86theorem access_cost_pos_of_nonzero (d : ℕ) (hd : 0 < d) :
  87    0 < Jcost (phi ^ d) := by
  88  rw [← access_cost_zero_at_origin]
  89  exact Jcost_phi_pow_strictMono hd
  90
  91/-! ## Part 4: Collocation Minimizes Cost -/
  92
  93/-- **COLLOCATION MINIMIZES COST**: Distance 0 beats any nonzero distance. -/
  94theorem collocation_minimizes_cost (d : ℕ) (hd : 0 < d) :
  95    Jcost (phi ^ 0) < Jcost (phi ^ d) :=