trajectory_at_equilibrium
plain-language theorem explainer
Any self-map f on positive reals that fixes the equilibrium ratio 1 and strictly decreases J-cost away from it keeps the iterated trajectory starting at 1 fixed at 1 for every step count. Control engineers verifying PID closed-loop behavior around a setpoint would cite the result when confirming that a tuned controller cannot drift from the canonical fixed point. The argument is a direct induction on the iteration count that invokes the fixed-point axiom at the base and the successor unfolding together with the fixes_equilibrium field at each 1
Claim. Let $f : (0,∞) → (0,∞)$ be a map that fixes the point 1 and satisfies $J(f(r)) < J(r)$ whenever $r > 0$ and $r ≠ 1$. Then the $n$-fold iterate of $f$ applied to the initial ratio 1 equals 1 for every natural number $n$.
background
RecognitionDescent is the structure that encodes the essential stability property of a PID-class controller in J-cost language: the map fixes the equilibrium ratio 1 and strictly lowers J-cost at every off-equilibrium positive ratio. The trajectory function is the forward orbit obtained by repeated application of the controller, defined recursively by trajectory f r 0 = r and trajectory f r (n+1) = f (trajectory f r n). The module situates this inside the broader claim that closed-loop PID stability around a setpoint is equivalent to monotone descent of J-cost on the realised-to-setpoint ratio, with termination exactly at ratio 1 because J-cost vanishes if and only if the argument equals 1.
proof idea
The proof proceeds by induction on n. The base case n = 0 is immediate from the definition of trajectory at step zero. In the successor step the successor unfolding of trajectory is substituted, the inductive hypothesis replaces the inner trajectory by 1, and the fixes_equilibrium field of the RecognitionDescent hypothesis supplies the required equality f 1 = 1.
why it matters
The result supplies the trajectory_fixes_equilibrium field inside the pidStabilityCert certificate, which in turn assembles the full structural theorem that any RecognitionDescent controller produces a J-cost sequence that is monotone non-increasing and terminates precisely at equilibrium. It therefore closes one link in the chain that reduces PID stability to the Recognition Composition Law and the uniqueness of the J-function. The declaration touches the open question of which concrete gain schedules (Ziegler-Nichols, SIMC, AMIGO) realise RecognitionDescent for a given plant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.