local_minimum
plain-language theorem explainer
The result establishes that the J-cost function is strictly positive for every positive real number different from one. Researchers deriving optimization problems from Recognition Science would cite this to confirm that local minima occur at positive cost values away from equilibrium. The argument is a direct application of the upstream positivity lemma for the J-cost.
Claim. For every real number $r$ with $r > 0$ and $r ≠ 1$, the J-cost function satisfies $J(r) > 0$.
background
The module recasts optimization as J-cost minimization, with five canonical problem types identified with spatial dimension D = 5. Global minimum occurs where J-cost reaches zero at recognition equilibrium; local minimum occurs where J-cost remains positive. The upstream lemma states: 'J(x) > 0 for x ≠ 1 and x > 0.' This supplies the local-minimum ingredient under the module's conventions that all optimization reduces to J-cost minimization.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one to the hypotheses 0 < r and r ≠ 1.
why it matters
This declaration populates the local_min field of optimizationTheoryCert, which certifies the full optimization theory by assembling five problem types, global minimum, and local minimum. It implements the Recognition Science claim that optimization equals J-cost minimization, separating local optima (J > 0) from global equilibrium (J = 0). No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.