IndisputableMonolith.Mathematics.OptimizationProblemClassesFromConfigDim
This module defines classes of optimization problems indexed by configuration dimension in the Recognition Science setting. Researchers formalizing discrete optimization within the RS framework would reference these type definitions. It consists solely of definitions and counts with no proofs or theorems.
claimLet $d$ be configuration dimension. Define optimization problem classes $C_d$ together with a count function and a certification predicate $Cert(C_d)$ that records membership in the class.
background
The module sits in the Mathematics domain and imports Mathlib plus IndisputableMonolith.Constants. The sole upstream import supplies the RS-native time quantum with doc-comment stating that τ₀ equals one tick. Sibling declarations introduce OptimizationClass, an associated count, OptimizationClassesCert, and its certifying function, all parameterized by configuration dimension.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the base type definitions for optimization classes indexed by dimension. These feed into later Recognition Science constructions that connect discrete optimization to the forcing chain T0-T8 and the phi-ladder. No downstream uses are recorded in the current dependency graph.
scope and limits
- Does not prove any properties of the defined classes.
- Does not relate the classes to specific RS constants such as phi or alpha.
- Does not specify how configuration dimension is computed from the phi-ladder.
- Does not provide examples or instances of the classes.