trajectory_succ
plain-language theorem explainer
The successor clause for the discrete trajectory of a state ratio r under controller map f states that trajectory f r (n+1) equals f applied to the prior state. Control theorists formalizing PID closed-loop behavior cite this when inducting over time steps to establish descent or invariance properties. The proof is a one-line reflexivity that matches the recursive clause in the definition of trajectory.
Claim. For any controller map $f : {R} {to} {R}$, initial ratio $r {in} {R}$, and step $n {in} {N}$, the trajectory satisfies trajectory$(f, r, n+1) = f($trajectory$(f, r, n))$.
background
The PIDStabilityFromJCost module models closed-loop PID dynamics via the realised-to-setpoint ratio r. A controller is abstracted as a self-map f that must satisfy RecognitionDescent: it fixes the equilibrium at r=1 and strictly decreases J-cost off equilibrium. The trajectory is the orbit obtained by iterating f, with base case trajectory f r 0 = r and successor trajectory f r (n+1) = f(trajectory f r n).
proof idea
The proof is a one-line term-mode reflexivity that directly unfolds the successor clause of the upstream trajectory definition.
why it matters
This supplies the inductive step used by trajectory_at_equilibrium (which shows invariance at r=1 under RecognitionDescent) and trajectory_pos (which shows positivity is preserved). It therefore supports the module's structural claim that PID stability reduces to monotone J-cost descent on the ratio, the discrete-time counterpart of the Recognition Composition Law and J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.