costRateEL_implies_const_one

formal source

  71    This is the rigidity statement: the only critical points of the
  72    cost-rate action among admissible paths are constants at the cost
  73    minimum. -/
  74theorem costRateEL_implies_const_one (γ : ℝ → ℝ) (hpos : ∀ t, 0 < γ t)
  75    (hEL : costRateELHolds γ) : ∀ t, γ t = 1 := by
  76  intro t
  77  -- J'(x) = (1 - x⁻²)/2 = 0 ↔ x⁻² = 1 ↔ x² = 1 ↔ (since x > 0) x = 1.
  78  have hd := hEL t
  79  have hpost : 0 < γ t := hpos t
  80  have hd' := IndisputableMonolith.Cost.deriv_Jcost hpost
  81  rw [hd'] at hd
  82  unfold IndisputableMonolith.Cost.JcostDeriv at hd
  83  -- (1 - (γ t)⁻²)/2 = 0 → (γ t)⁻² = 1
  84  have h1 : 1 - (γ t) ^ (-2 : ℤ) = 0 := by linarith
  85  have h2 : (γ t) ^ (-2 : ℤ) = 1 := by linarith
  86  -- (γ t)⁻² = 1 → γ t = 1 (since γ t > 0)
  87  have hne : γ t ≠ 0 := ne_of_gt hpost
  88  have h3 : (γ t) ^ (2 : ℤ) = 1 := by
  89    have hinv : (γ t) ^ (-2 : ℤ) = ((γ t) ^ (2 : ℤ))⁻¹ := by
  90      rw [zpow_neg]
  91    rw [hinv] at h2
  92    have hpow_pos : 0 < (γ t) ^ (2 : ℤ) := by positivity
  93    have hpow_ne : (γ t) ^ (2 : ℤ) ≠ 0 := ne_of_gt hpow_pos
  94    field_simp at h2
  95    exact h2.symm
  96  have h4 : (γ t) ^ 2 = 1 := by
  97    have : (γ t) ^ (2 : ℤ) = (γ t) ^ (2 : ℕ) := by norm_cast
  98    rw [this] at h3
  99    exact_mod_cast h3
 100  -- γ t > 0 and (γ t)² = 1 → γ t = 1
 101  -- (γ t - 1)(γ t + 1) = γ t² - 1 = 0 → γ t = 1 (since γ t > 0)
 102  have h6 : (γ t - 1) * (γ t + 1) = 0 := by
 103    have : (γ t - 1) * (γ t + 1) = (γ t) ^ 2 - 1 := by ring
 104    rw [this, h4]; ring