PIDStabilityCert
PIDStabilityCert packages five properties that certify closed-loop stability for any controller map satisfying RecognitionDescent: equilibrium fixation, positive trajectories, trajectory fixation at 1, strict J-cost descent off equilibrium, and the zero-cost equivalence at 1. Control theorists formalizing model-free PID proofs cite it to link J-cost descent to setpoint convergence. The declaration is a structure definition that assembles the fixes, trajectory, and cost lemmas proved earlier in the same module.
claimA PID stability certificate is a record containing five assertions for self-maps $f : ℝ → ℝ$ satisfying RecognitionDescent: (i) $f(1) = 1$; (ii) every trajectory starting at $r > 0$ remains positive; (iii) the trajectory starting at 1 remains fixed at 1 for all steps; (iv) $Jcost(f(r)) < Jcost(r)$ whenever $r > 0$ and $r ≠ 1$; (v) $Jcost(x) = 0$ if and only if $x = 1$ for $x > 0$.
background
The J-cost (Cost.Jcost) is the recognition cost function supplied by the RSNative.Core abbrev; it vanishes exactly at the equilibrium ratio 1 and is strictly positive elsewhere for positive arguments. RecognitionDescent is the structure asserting that a self-map $f$ fixes 1, preserves positivity, and strictly decreases J-cost off equilibrium. The trajectory function iterates the map: trajectory $f$ $r$ 0 = $r$ and trajectory $f$ $r$ ($n+1$) = $f$(trajectory $f$ $r$ $n$).
proof idea
This declaration is a structure definition with no proof body. It directly assembles the five fields by referencing the already-proved lemmas: fixes_equilibrium from RecognitionDescent, preserves_positive_traj from trajectory_pos, trajectory_fixes_equilibrium from trajectory_at_equilibrium, cost_descent_off_equilibrium from cost_descent_step, and cost_zero_iff_equilibrium from the local theorem of the same name.
why it matters in Recognition Science
The structure is the master certificate in §6 of the module and is instantiated by pidStabilityCert. It formalizes the reduction of PID-class stability to monotone J-cost descent, treating RecognitionDescent as the unifying signature independent of gain-tuning method. The result packages the abstract descent properties into a single record usable for downstream stability arguments in the Recognition Science framework.
scope and limits
- Does not construct an explicit RecognitionDescent map for any physical plant.
- Does not address discretization, sampling, or actuator limits.
- Does not derive quantitative bounds on convergence rate or overshoot.
- Does not extend to multi-variable or nonlinear plant models.
formal statement (Lean)
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