102theorem trajectory_at_equilibrium {f : ℝ → ℝ} 103 (hf : RecognitionDescent f) (n : ℕ) : trajectory f 1 n = 1 := by
proof body
Term-mode proof.
104 induction n with 105 | zero => rfl 106 | succ k ih => rw [trajectory_succ, ih]; exact hf.fixes_equilibrium 107 108/-! ## §4. J-cost descent under iteration -/ 109 110/-- If the controller exhibits recognition descent and the trajectory 111preserves positivity (which it does, by `preserves_positive`), then 112the per-step J-cost is non-increasing. Strict descent holds whenever 113the current state is off equilibrium. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.