RecognitionDescent
plain-language theorem explainer
RecognitionDescent encodes the property that a self-map f fixes the equilibrium ratio 1 and strictly decreases J-cost off equilibrium. Control engineers cite it when certifying that a PID loop is stable by monotone descent on the recognition cost. The definition consists of three fields with no proof obligations.
Claim. A map $f : ℝ → ℝ$ exhibits recognition descent when $f(1) = 1$, $f$ maps positive reals to positive reals, and $Jcost(f(r)) < Jcost(r)$ for every $r > 0$ with $r ≠ 1$.
background
In the PIDStabilityFromJCost module the J-cost is the function Cost.Jcost drawn from the RSNative Core, satisfying Jcost(1) = 0 and Jcost(x) > 0 precisely when x ≠ 1 for x > 0. The trajectory function iterates any controller map by trajectory f r 0 = r and trajectory f r (n+1) = f (trajectory f r n). The module states that closed-loop stability of a PID controller around a setpoint reduces to monotone J-cost descent on the realised/setpoint ratio r.
proof idea
The declaration is a structure definition with three fields. fixes_equilibrium asserts f 1 = 1. preserves_positive requires that 0 < r implies 0 < f r. strict_descent_off encodes the strict inequality Cost.Jcost (f r) < Cost.Jcost r whenever 0 < r and r ≠ 1. No lemmas are invoked; downstream results such as cost_descent_step simply project the strict_descent_off field.
why it matters
RecognitionDescent supplies the central hypothesis for PIDStabilityCert, pid_stability_one_statement, trajectory_at_equilibrium and cost_descent_step. It formalises the structural signature of any adequately-tuned PID-class controller, independent of Ziegler-Nichols or SIMC tuning, and links directly to J-uniqueness (T5) in the forcing chain. The definition closes the abstract layer before domain-specific realisations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.