trajectory
plain-language theorem explainer
The definition constructs the discrete sequence of state ratios obtained by iterating a controller map f on an initial ratio r. Control theorists formalizing PID stability via J-cost descent cite it to index the closed-loop trajectory along which monotonicity is proved. The definition is the standard recursive unfolding with base case at step zero and successor step given by one application of f.
Claim. Let $f : {R} {to} {R}$ be a controller map and let $r {in} {R}$ be an initial realized-to-setpoint ratio. The trajectory is the sequence $(x_n)_{n {in} {N}}$ defined by $x_0 := r$ and $x_{n+1} := f(x_n)$.
background
The PIDStabilityFromJCost module reduces closed-loop stability of a PID controller to monotone descent of the J-cost on the realized/setpoint ratio. The J-cost, imported from the Cost module, is the function $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$, which vanishes exactly at the equilibrium $x = 1$ and is strictly positive elsewhere. The module doc-comment states that any controller satisfying the RecognitionDescent property generates a sequence whose J-costs are strictly monotone decreasing and terminate at equilibrium.
proof idea
The definition is given directly by pattern matching on the natural-number index: the base case at 0 returns the initial ratio r, and the successor case applies the controller map f to the value at the predecessor index. No lemmas or tactics are invoked; it is the standard inductive definition of function iteration.
why it matters
This definition supplies the sequence along which the RecognitionDescent property is applied in forty downstream declarations, including the energy-conservation theorem under time-translation symmetry and the rigidity result that cost-rate Euler-Lagrange paths are constant at the J-cost minimum. It fills the structural slot in the module doc-comment that links PID tuning regimes (Ziegler-Nichols, AMIGO, SIMC) to the Recognition Science J-cost descent, thereby connecting robotics control to the T5 J-uniqueness and T6 phi fixed-point landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.