cost_zero_iff_equilibrium
plain-language theorem explainer
The theorem states that for positive real x the J-cost vanishes if and only if x equals one. PID stability proofs cite the equivalence to confirm that J-cost descent terminates only at the setpoint ratio. The term-mode proof splits the biconditional, using the strict-positivity lemma for the forward direction and direct substitution for the reverse.
Claim. For every real number $x > 0$, the J-cost satisfies $J(x) = 0$ if and only if $x = 1$.
background
The J-cost is defined in the Cost module as $J(x) = (x-1)^2/(2x)$ for $x > 0$. RecognitionDescent is the structure on a self-map $f : ℝ → ℝ$ that fixes the point at one, preserves positivity, and strictly decreases J-cost off equilibrium. The module sets the local setting for PID controllers by reducing closed-loop stability to monotone descent on the realised-to-setpoint ratio under this property.
proof idea
The term proof refines a pair of implications. The left-to-right direction assumes Jcost x = 0, derives a contradiction from x ≠ 1 via the upstream lemma Jcost_pos_of_ne_one together with linarith. The right-to-left direction rewrites the hypothesis x = 1 and applies the upstream unit lemma Jcost_unit0.
why it matters
The result supplies the zero-cost characterisation required by the downstream PIDStabilityCert and the packaged pid_stability_one_statement. It instantiates J-uniqueness for the robotics extension, ensuring that any RecognitionDescent trajectory reaches the unique point where the controller exerts no further drive. The equivalence closes the structural argument that descent on J-cost is the unifying signature of tuned PID-class controllers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.