optimizationTheoryCert
plain-language theorem explainer
optimizationTheoryCert packages the core claims of Recognition Science optimization into a single certificate: exactly five problem types, global J-cost minimum of zero at argument one, and strict positivity of J-cost away from one. A researcher deriving optimization results from the J-cost functional equation would cite this to anchor the five-type classification to configDim D. The definition is a direct structure constructor that wires in the pre-established cardinality theorem and the two J-cost minimum theorems.
Claim. The optimization theory certificate asserts that the set of optimization problem types has cardinality five, that the J-cost function satisfies $J(1)=0$, and that $J(r)>0$ for every real $r>0$ with $r≠1$.
background
The module presents optimization theory extracted from Recognition Science as J-cost minimization. Five canonical types (linear, nonlinear, combinatorial, convex, stochastic) are identified with configuration dimension D=5. Global minimum occurs at J=0 (recognition equilibrium); local minima satisfy J>0 but remain locally optimal. KKT conditions are likewise counted as five constraint-active cases matching D.
proof idea
The definition is a direct structure instantiation of OptimizationTheoryCert. It assigns the five_types field to the theorem optimizationProblemTypeCount, the global_min field to the theorem global_minimum, and the local_min field to the theorem local_minimum. No additional tactics or reductions occur.
why it matters
This definition closes the packaging of the five-type optimization claims inside the Recognition Science framework, where all optimization reduces to J-cost minimization with equilibrium at J=0. It supplies the concrete certificate referenced by the module's statement that Lean status is zero sorry and zero axiom. No downstream uses are recorded, leaving open whether the certificate will be invoked in later derivations of KKT conditions or convergence results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.