optimizationClassesCert
plain-language theorem explainer
The declaration constructs a certificate asserting that exactly five optimization problem classes arise from the configuration dimension. Operations researchers formalizing problem taxonomies would reference this when verifying classification completeness. It is realized as a direct structure instantiation that substitutes the decidable cardinality theorem into the required field.
Claim. Let $C$ be the finite type of optimization problem classes. Then optimizationClassesCert is the structure of type OptimizationClassesCert whose field five_classes equals the theorem establishing $|C| = 5$.
background
The module sets configDim to 5 and identifies five canonical optimization classes: linear, convex nonlinear, integer, stochastic, and dynamic. The structure OptimizationClassesCert packages the single assertion that the cardinality of the type OptimizationClass is exactly 5. The upstream theorem optimizationClass_count establishes this equality by direct computation via the decide tactic, confirming the enumeration without additional hypotheses.
proof idea
The definition is a one-line wrapper that applies the theorem optimizationClass_count to populate the five_classes field of the OptimizationClassesCert structure.
why it matters
This definition supplies the concrete certificate for the five-class taxonomy derived from configDim, closing the classification step in the optimization layer. It aligns with the forcing chain where dimensional parameters are fixed by self-similar structures, though it does not yet connect to downstream uses in physical modeling. No open questions are addressed here beyond the cardinality verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.