OptimizationTheoryCert
plain-language theorem explainer
This structure packages a certificate asserting five optimization problem types, global J-cost minimum of zero at argument 1, and strict positivity of J-cost for all other positive arguments. Researchers deriving optimization results from Recognition Science would cite it to anchor the claim that all optimization reduces to J-cost minimization with configDim equal to 5. The declaration is a direct structure bundling the three properties with no additional proof obligations.
Claim. Let $J$ be the J-cost function. The structure certifies that the set of optimization problem types has cardinality 5 (linear, nonlinear, combinatorial, convex, stochastic), that $J(1)=0$, and that $J(r)>0$ for every real $r>0$ with $r≠1$.
background
The module states that optimization in Recognition Science is J-cost minimization, with global minimum at recognition equilibrium (J=0) and local minima satisfying J>0. The five problem types are defined inductively as linear, nonlinear, combinatorial, convex, stochastic; this inductive type derives Fintype, enabling the cardinality assertion. J-cost is imported from the Cost module and measures deviation from equilibrium.
proof idea
The declaration is a structure definition that directly bundles the cardinality fact, the global minimum equation, and the local minimum positivity condition. It functions as a one-line wrapper collecting these three properties for use in the downstream certificate construction.
why it matters
The structure is instantiated by the downstream definition optimizationTheoryCert, which supplies the concrete values for the five-type count, global minimum, and local minimum. It supports the module claim that KKT conditions correspond to the five constraint-active cases and that configDim D equals 5. In the Recognition framework it grounds the reduction of optimization to J-cost minimization under the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.