PIDStabilityCert
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.