optimizationClass_count
plain-language theorem explainer
The result asserts that the finite set of optimization problem classes has exactly five elements when the configuration dimension equals five. Operations researchers applying the Recognition Science model would reference this enumeration to align with the five canonical classes: linear, convex nonlinear, integer, stochastic, and dynamic. The proof is a direct computation via the decide tactic on the Fintype instance of the inductive type.
Claim. The cardinality of the type of optimization classes is five: $|$OptimizationClass$| = 5$.
background
The module defines five canonical optimization classes corresponding to configDim equal to five. These are linear, convex nonlinear, integer, stochastic, and dynamic problems. The inductive type OptimizationClass enumerates them explicitly, deriving Fintype, DecidableEq, and related instances. This setup provides the mathematical foundation for certifying optimization problem classifications in the Recognition Science framework.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to compute the cardinality of the finite inductive type OptimizationClass.
why it matters
This theorem supplies the count used by optimizationClassesCert to construct the certification record. It directly implements the module's claim that five classes arise from configDim D = 5. In the broader framework, it supports the mapping from configuration dimensions to problem classes without invoking the forcing chain or phi-ladder structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.