global_minimum
plain-language theorem explainer
The theorem establishes that the J-cost function attains its global minimum value of zero at argument one. Researchers deriving optimization equilibria from recognition costs would cite this when anchoring J-minimization frameworks. The proof is a direct one-line term application of the upstream Jcost_unit0 lemma.
Claim. The J-cost function, given by $J(x) = (x-1)^2/(2x)$, satisfies $J(1) = 0$.
background
The Optimization Theory from RS module frames all optimization problems as J-cost minimizations, with five canonical types matching configDim D = 5. Global minimum corresponds to recognition equilibrium (J = 0) while local minima satisfy J > 0. The J-cost is defined explicitly as the squared ratio $J(x) = (x-1)^2/(2x)$, per the upstream lemma.
proof idea
The proof is a term-mode one-liner that directly invokes the Jcost_unit0 lemma from the Cost module. That lemma reduces the claim to simplification of the J-cost definition.
why it matters
This result populates the global_min field inside optimizationTheoryCert, which bundles the five problem types with global and local minimum properties. It supplies the base equilibrium case for the RS claim that optimization reduces to J-cost minimization, aligning with recognition equilibrium in the broader forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.