cost_descent_step
plain-language theorem explainer
Any recognition-descent map f strictly lowers J-cost on every positive ratio r away from unity. Control theorists cite the result to certify that a PID controller whose action satisfies RecognitionDescent produces a monotone-decreasing J-cost sequence that terminates only at equilibrium. The proof is a one-line field projection onto the strict_descent_off axiom of the RecognitionDescent structure.
Claim. Let $f : (0,∞) → (0,∞)$ satisfy the recognition-descent axioms (fixes the point 1 and strictly decreases J-cost off that point). Then for every $r > 0$ with $r ≠ 1$, $J(f(r)) < J(r)$.
background
RecognitionDescent is the structure on a self-map f : ℝ → ℝ that requires f(1) = 1 together with the strict inequality Jcost(f r) < Jcost r for all r > 0, r ≠ 1. Jcost itself is the non-negative cost function induced by the multiplicative recognizer comparator; it vanishes if and only if its argument equals 1. The module treats a PID controller as an iteration of such an f on the realised-to-setpoint ratio, so that closed-loop stability reduces to monotone descent of this cost.
proof idea
The proof is the one-line wrapper that applies the strict_descent_off field of the hypothesis hf : RecognitionDescent f directly to the supplied r, hr and hne.
why it matters
The declaration supplies the descent step consumed by pidStabilityCert, which assembles the full PIDStabilityCert record (fixes equilibrium, preserves positivity of trajectories, and certifies cost descent off equilibrium). It thereby completes the abstract stability argument of the module, connecting the RecognitionDescent property to the J-cost uniqueness result Jcost x = 0 ↔ x = 1 that follows from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.