pidStabilityCert
plain-language theorem explainer
The stability certificate assembles a complete record showing that any map satisfying recognition descent stabilizes the state ratio at equilibrium through strict J-cost decrease at each step. Control theorists would cite this construction when reducing PID closed-loop behavior to the abstract descent property. The definition proceeds by record construction that directly invokes the supporting lemmas for each certificate field.
Claim. The stability certificate structure has fields asserting that every recognition descent map $f$ satisfies $f(1)=1$, that trajectories from positive initial ratios remain positive, that the trajectory starting at one remains fixed at one, that the J-cost decreases strictly when off equilibrium, and that the J-cost is zero precisely at equilibrium for positive ratios. The concrete instance is realized by delegating each assertion to the trajectory and descent lemmas.
background
The module shows that closed-loop stability of a PID controller reduces to monotone J-cost descent on the realized-to-setpoint ratio. Recognition descent is the property that a self-map on the positive reals strictly decreases the J-cost function off equilibrium and fixes the equilibrium point at one. The trajectory function generates the sequence of states under repeated application of the map. From the module documentation: 'If the realised state ratio r := output / setpoint is at the canonical equilibrium r = 1, the J-cost vanishes (Jcost 1 = 0) and the controller has nothing to drive (δr = 0).'
proof idea
The definition constructs the stability certificate record by assigning each field to a lemma from the same module. The equilibrium fixation field delegates to the corresponding component of the recognition descent hypothesis. The positive trajectory field invokes the positivity preservation lemma. The equilibrium trajectory field invokes the fixation lemma. The cost descent field invokes the strict descent step lemma. The zero-cost equivalence field invokes the zero-cost equivalence lemma. This is a direct structural assembly without additional reasoning steps.
why it matters
This declaration completes the master certificate for PID stability derived from J-cost descent in the robotics module. It packages the abstract properties that any adequately tuned PID controller must satisfy, independent of the specific tuning method. Within Recognition Science it realizes the descent property that follows from the forcing chain and the uniqueness of the J function at the self-similar fixed point. The certificate has no downstream uses yet but provides the interface for concrete controller models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.