cost_pos_off_equilibrium
plain-language theorem explainer
For positive real x not equal to one the J-cost is strictly positive. Control engineers modeling PID loops around a setpoint would cite this to confirm that any deviation from equilibrium incurs positive recognition cost. The proof is a direct one-line application of the core J-cost positivity lemma.
Claim. For every real number $x > 0$ with $x ≠ 1$, the J-cost satisfies $J(x) > 0$.
background
The module develops an abstract stability certificate for PID-class controllers by showing that closed-loop behavior reduces to monotone descent of the J-cost on the realized-to-setpoint ratio. Equilibrium occurs exactly at ratio one, where J-cost vanishes; the present result supplies the contrapositive that any other positive ratio carries strictly positive cost. This pairs with the RecognitionDescent property to guarantee that iterated application drives the ratio to one and terminates there.
proof idea
One-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module, passing the hypotheses that x is positive and unequal to one.
why it matters
The result supplies the missing half of the equilibrium characterization required by the PID stability master certificate. It ensures that RecognitionDescent terminates only at the fixed point r = 1, consistent with the J-uniqueness step (T5) and the eight-tick octave structure of the forcing chain. The module doc-comment explicitly positions this positivity as the structural signature unifying Ziegler-Nichols, AMIGO and SIMC tuning regimes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.