OptimizationProblemType
plain-language theorem explainer
The inductive definition OptimizationProblemType enumerates five canonical optimization problem categories in the Recognition Science setting. A researcher mapping J-cost minimization onto classical optimization classes would cite this enumeration to anchor the configDim D = 5 correspondence. The declaration is a direct inductive construction that automatically derives decidable equality, representation, and finiteness.
Claim. The set of optimization problem types is the finite collection consisting of the five elements linear, nonlinear, combinatorial, convex, and stochastic.
background
The module states that all optimization reduces to J-cost minimization, with the global minimum at J = 0 (recognition equilibrium) and local minima satisfying J > 0 while remaining locally optimal. KKT conditions are grouped into five types of active constraints, matching the configuration dimension D = 5. The J-cost itself originates from the Recognition Composition Law in the imported Cost module.
proof idea
The declaration is the inductive definition that introduces the five constructors linear, nonlinear, combinatorial, convex, and stochastic, together with the derived instances for DecidableEq, Repr, BEq, and Fintype.
why it matters
This definition supplies the five problem types required by the downstream theorem optimizationProblemTypeCount, which proves that the cardinality is exactly 5, and by the structure OptimizationTheoryCert that records the global minimum Jcost 1 = 0 together with the local-minimum property. It fills the configDim D = 5 slot that links the five KKT constraint classes to the broader reduction of optimization to J-cost minimization in the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.