trajectory_zero
plain-language theorem explainer
The base case of the state trajectory under repeated controller application states that zero iterations leave the initial ratio unchanged. Researchers formalizing J-cost descent for PID controllers would cite this when initializing inductive arguments on the trajectory sequence. The proof is a direct reflexivity on the recursive definition of trajectory.
Claim. For any controller map $f : ℝ → ℝ$ and initial ratio $r ∈ ℝ$, the trajectory at step zero satisfies trajectory$(f,r,0) = r$.
background
In the PID stability module the trajectory function models evolution of the realized-to-setpoint ratio under iterated application of a controller map. It is defined recursively with the base case returning the initial ratio and the successor case applying the map to the prior state. The module shows that closed-loop PID stability reduces to monotone J-cost descent on this ratio, with equilibrium fixed at ratio 1 where J-cost vanishes. The upstream definition states: 'The state trajectory under repeated controller application.'
proof idea
The proof is a one-line wrapper that applies the base case of the recursive definition of the trajectory function.
why it matters
This base case anchors the trajectory sequence used to prove J-cost descent for PID controllers. It supports sibling results such as trajectory_succ and cost_descent_step that together establish RecognitionDescent implies strict monotone decrease until equilibrium at r=1. It fills the initial step in the structural theorem linking PID tuning to J-cost properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.