pid_stability_one_statement
plain-language theorem explainer
Any map f : ℝ → ℝ satisfying recognition descent fixes the equilibrium ratio at 1, strictly decreases J-cost for every positive ratio away from 1, and has J-cost vanishing exactly at equilibrium. Control theorists working with PID tuning cite this as the abstract stability certificate reducing closed-loop behavior to monotone J-cost descent. The proof is a direct extraction that pulls the fixes and strict-descent clauses from the RecognitionDescent structure and applies the cost-zero equivalence lemma.
Claim. Let $f : ℝ → ℝ$ satisfy recognition descent. Then $f(1) = 1$, for all $r > 0$ with $r ≠ 1$ one has $J(f(r)) < J(r)$, and for all $x > 0$ one has $J(x) = 0$ if and only if $x = 1$, where $J$ denotes the J-cost function.
background
The module develops an abstract stability certificate for PID controllers by reducing closed-loop behavior to descent on the J-cost function. RecognitionDescent f is the structure requiring that f fixes the equilibrium ratio 1, preserves positivity of the iterated trajectory, and strictly lowers J-cost at every off-equilibrium positive ratio. The J-cost itself is the recognition functional pulled from the core measurement module, with the equivalence Jcost x = 0 ↔ x = 1 for x > 0 established upstream by cost_zero_iff_equilibrium.
proof idea
The proof introduces f and the hypothesis hf : RecognitionDescent f. It refines the goal into the triple consisting of hf.fixes_equilibrium, the strict_descent_off clause extracted from hf, and the cost_zero_iff_equilibrium lemma applied under the positivity assumption.
why it matters
This supplies the compact one-statement packaging of the PID stability properties collected in the PIDStabilityCert structure of the same module. It instantiates the J-cost descent mechanism as the unifying signature for any adequately tuned PID controller, independent of specific gain rules. The result closes the abstract argument in the robotics extension of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.