RecognitionDescent

formal source

  79  (i) it fixes the equilibrium `r = 1`, and
  80  (ii) for every `r ∈ (0, ∞) \ {1}`, the J-cost strictly decreases:
  81      `Jcost (f r) < Jcost r`. -/
  82structure RecognitionDescent (f : ℝ → ℝ) : Prop where
  83  fixes_equilibrium : f 1 = 1
  84  preserves_positive : ∀ r : ℝ, 0 < r → 0 < f r
  85  strict_descent_off :
  86    ∀ r : ℝ, 0 < r → r ≠ 1 → Cost.Jcost (f r) < Cost.Jcost r
  87
  88/-! ## §2. Iterating the controller -/
  89
  90/-- The state trajectory under repeated controller application. -/
  91def trajectory (f : ℝ → ℝ) (r : ℝ) : ℕ → ℝ
  92  | 0 => r
  93  | n + 1 => f (trajectory f r n)
  94
  95theorem trajectory_zero (f : ℝ → ℝ) (r : ℝ) : trajectory f r 0 = r := rfl
  96
  97theorem trajectory_succ (f : ℝ → ℝ) (r : ℝ) (n : ℕ) :
  98    trajectory f r (n + 1) = f (trajectory f r n) := rfl
  99
 100/-! ## §3. Equilibrium fixed point -/
 101
 102theorem trajectory_at_equilibrium {f : ℝ → ℝ}
 103    (hf : RecognitionDescent f) (n : ℕ) : trajectory f 1 n = 1 := by
 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