theorem
proved
tactic proof
costRateEL_implies_const_one
show as:
view Lean formalization →
formal statement (Lean)
74theorem costRateEL_implies_const_one (γ : ℝ → ℝ) (hpos : ∀ t, 0 < γ t)
75 (hEL : costRateELHolds γ) : ∀ t, γ t = 1 := by
proof body
Tactic-mode proof.
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
105 have hsum_pos : 0 < γ t + 1 := by linarith
106 have hsum_ne : γ t + 1 ≠ 0 := ne_of_gt hsum_pos
107 have h7 : γ t - 1 = 0 := by
108 rcases mul_eq_zero.mp h6 with h | h
109 · exact h
110 · exact absurd h hsum_ne
111 linarith
112
113/-- **Equivalence: cost-rate EL holds iff the path is constantly at `1`.**
114
115 Among admissible (positive, continuous) paths, the constant ground
116 state `γ ≡ 1` is the *unique* solution of the cost-rate EL equation.
117 This is the cleanest possible "principle of least action": there is
118 exactly one trajectory in the cost manifold that has no first-order
119 cost change at every point, and it is the path that stays at the
120 cost minimum forever. -/