trajectory_pos
plain-language theorem explainer
trajectory_pos asserts that any trajectory generated by a recognition-descent map stays strictly positive when begun from a positive initial ratio. PID stability analysts cite it to guarantee that the realised-to-setpoint sequence never leaves the domain where J-cost is defined and positive off equilibrium. The argument is a direct induction on iteration count that invokes the preserves_positive field of RecognitionDescent at each successor step.
Claim. Let $f : ℝ → ℝ$ satisfy recognition descent. For any initial ratio $r > 0$ and any $n ∈ ℕ$, the $n$-step trajectory satisfies trajectory$(f, r, n) > 0$, where trajectory$(f, r, 0) := r$ and trajectory$(f, r, n+1) := f($trajectory$(f, r, n))$.
background
RecognitionDescent is the structure on a self-map $f : ℝ → ℝ$ that fixes the equilibrium at 1, preserves positivity on positive inputs, and strictly decreases J-cost off equilibrium. The trajectory is the sequence obtained by iterating $f$ on an initial ratio $r$. The module treats recognition descent as the abstract signature of any adequately tuned PID-class controller, independent of specific gain rules such as Ziegler-Nichols or SIMC.
proof idea
The proof proceeds by induction on $n$. The base case $n = 0$ is immediate from the hypothesis $0 < r$. In the successor case, trajectory_succ rewrites the value at $n+1$ as $f$ applied to the prior trajectory value, after which the preserves_positive field of the RecognitionDescent hypothesis is applied directly to the inductive hypothesis.
why it matters
trajectory_pos supplies the preserves_positive_traj component inside pidStabilityCert, the top-level stability certificate for the module. It ensures the entire trajectory remains in the positive reals so that J-cost remains defined and the monotone descent argument can terminate only at equilibrium. Within the Recognition Science framework it supplies the positivity half of the iterated map that underlies the eight-tick octave and the reduction to $D = 3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.