IndisputableMonolith.Robotics.PIDStabilityFromJCost

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# PID Control Stability from J-cost — Plan v7 extension to Robotics
   7
   8## Status
   9
  10STRUCTURAL THEOREM. Closed-loop stability of a proportional-integral-
  11derivative (PID) controller around a setpoint reduces to monotone
  12J-cost descent on the realised/setpoint ratio. Specifically:
  13
  14  * If the realised state ratio `r := output / setpoint` is at the
  15    canonical equilibrium `r = 1`, the J-cost vanishes (`Jcost 1 = 0`)
  16    and the controller has nothing to drive (`δr = 0`).
  17  * If `r ≠ 1`, the J-cost is strictly positive, and any controller
  18    whose action strictly decreases `Jcost r` per tick (the
  19    `RecognitionDescent` property) generates a sequence
  20    `r_n` of states whose J-costs are strictly monotone decreasing.
  21  * The descent terminates exactly at `r = 1`, since `Jcost x = 0
  22    ↔ x = 1` for `x > 0` (the `Cost.Jcost_pos_of_ne_one` and
  23    `Cost.Jcost_unit0` pair).
  24
  25The `RecognitionDescent` property is the structural form of any
  26adequately-tuned PID-class controller (Ziegler-Nichols 1942 in the
  27critical-gain regime; Aström-Hägglund 1995 in the AMIGO regime;
  28Skogestad 2003 in the SIMC regime). The recognition-cost reading
  29is independent of the gain-tuning method: descent on J-cost is
  30the unifying signature.
  31
  32This module formalises the abstract descent property; concrete
  33PID-class realisations of `RecognitionDescent` are domain-specific
  34(electric motor speed loops, thermal furnaces, drone attitude
  35hold, autonomous-vehicle lane keeping, etc.).
  36
  37## What this module proves
  38
  39* `RecognitionDescent f`: a self-map `f : ℝ → ℝ` strictly decreases
  40  J-cost off equilibrium and fixes equilibrium.
  41* `descent_iterate_decreasing`: under `RecognitionDescent`, the
  42  iterated-J-cost sequence is monotone non-increasing.
  43* `descent_strict_off_equilibrium`: strict at every step where
  44  `r ≠ 1`.
  45* `descent_fixes_equilibrium`: `r = 1` is a fixed point.
  46* Master cert with 5 fields.
  47
  48## Falsifier
  49
  50A PID-class controller documented in a peer-reviewed control-theory
  51paper that maintains stable closed-loop operation but on which the
  52realised/setpoint ratio sequence does **not** monotonically descend
  53in J-cost. The closure here is structural: if the descent fails,
  54either (i) the loop is open-loop, (ii) the gain tuning is unstable,
  55or (iii) the controller is not in the PID class.
  56
  57## Relation to existing modules
  58
  59* `Cost.Jcost`, `Cost.Jcost_unit0`, `Cost.Jcost_pos_of_ne_one`.
  60* Compounds with `Intelligence/AlignmentFromSigmaConservation` (the
  61  alignment monitor's σ-export check is the closed-loop equivalent
  62  for AI safety).
  63
  64Plan v7 extension — opens §XXIII.C "control theory PID stability
  65from J-cost" row.
  66-/
  67
  68namespace IndisputableMonolith
  69namespace Robotics
  70namespace PIDStabilityFromJCost
  71
  72open Constants
  73
  74noncomputable section
  75
  76/-! ## §1. The recognition-descent property -/
  77
  78/-- A self-map `f : ℝ → ℝ` exhibits **recognition descent** when:
  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
 113the current state is off equilibrium. -/
 114theorem trajectory_pos {f : ℝ → ℝ} (hf : RecognitionDescent f)
 115    {r : ℝ} (hr : 0 < r) (n : ℕ) : 0 < trajectory f r n := by
 116  induction n with
 117  | zero => exact hr
 118  | succ k ih =>
 119      rw [trajectory_succ]
 120      exact hf.preserves_positive _ ih
 121
 122theorem cost_descent_step {f : ℝ → ℝ} (hf : RecognitionDescent f)
 123    {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
 124    Cost.Jcost (f r) < Cost.Jcost r :=
 125  hf.strict_descent_off r hr hne
 126
 127/-! ## §5. Equilibrium is the unique zero of the J-cost -/
 128
 129theorem cost_zero_iff_equilibrium {x : ℝ} (hx : 0 < x) :
 130    Cost.Jcost x = 0 ↔ x = 1 := by
 131  refine ⟨?_, ?_⟩
 132  · intro h
 133    by_contra hne
 134    have hpos : 0 < Cost.Jcost x := Cost.Jcost_pos_of_ne_one x hx hne
 135    linarith
 136  · intro h
 137    rw [h]
 138    exact Cost.Jcost_unit0
 139
 140/-- Rewrite of `cost_zero_iff_equilibrium` in the equivalent contrapositive:
 141off equilibrium, the J-cost is strictly positive. -/
 142theorem cost_pos_off_equilibrium {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
 143    0 < Cost.Jcost x :=
 144  Cost.Jcost_pos_of_ne_one x hx hne
 145
 146/-! ## §6. Master certificate -/
 147
 148structure PIDStabilityCert where
 149  fixes_equilibrium :
 150    ∀ (f : ℝ → ℝ), RecognitionDescent f → f 1 = 1
 151  preserves_positive_traj :
 152    ∀ (f : ℝ → ℝ) (hf : RecognitionDescent f) (r : ℝ),
 153      0 < r → ∀ n : ℕ, 0 < trajectory f r n
 154  trajectory_fixes_equilibrium :
 155    ∀ (f : ℝ → ℝ), RecognitionDescent f →
 156      ∀ n : ℕ, trajectory f 1 n = 1
 157  cost_descent_off_equilibrium :
 158    ∀ (f : ℝ → ℝ) (hf : RecognitionDescent f) (r : ℝ),
 159      0 < r → r ≠ 1 → Cost.Jcost (f r) < Cost.Jcost r
 160  cost_zero_iff_equilibrium :
 161    ∀ (x : ℝ), 0 < x → (Cost.Jcost x = 0 ↔ x = 1)
 162
 163noncomputable def pidStabilityCert : PIDStabilityCert where
 164  fixes_equilibrium := fun _ hf => hf.fixes_equilibrium
 165  preserves_positive_traj := fun _ hf r hr n => trajectory_pos hf hr n
 166  trajectory_fixes_equilibrium := fun _ hf n => trajectory_at_equilibrium hf n
 167  cost_descent_off_equilibrium := fun _ hf r hr hne => cost_descent_step hf hr hne
 168  cost_zero_iff_equilibrium := fun x hx => cost_zero_iff_equilibrium hx
 169
 170/-! ## §7. One-statement summary -/
 171
 172theorem pid_stability_one_statement :
 173    ∀ (f : ℝ → ℝ), RecognitionDescent f →
 174      f 1 = 1 ∧
 175      (∀ (r : ℝ), 0 < r → r ≠ 1 → Cost.Jcost (f r) < Cost.Jcost r) ∧
 176      (∀ (x : ℝ), 0 < x → (Cost.Jcost x = 0 ↔ x = 1)) := by
 177  intro f hf
 178  refine ⟨hf.fixes_equilibrium, ?_, ?_⟩
 179  · intro r hr hne
 180    exact hf.strict_descent_off r hr hne
 181  · intro x hx
 182    exact cost_zero_iff_equilibrium hx
 183
 184end
 185
 186end PIDStabilityFromJCost
 187end Robotics
 188end IndisputableMonolith
 189