DiscreteConfigSpace
plain-language theorem explainer
DiscreteConfigSpace axiomatizes a finite set of positive reals equipped with a positive minimum defect gap that isolates the point 1 under the J-cost. Researchers proving stability of minima in Recognition Science cite this structure when moving from continuous drift to trapped configurations. The definition directly records the gap_property axiom on defect without further derivation.
Claim. A finite set $C subset (0, infty)$ together with $delta > 0$ such that for all $x in C$ with $x neq 1$, the defect satisfies $J(x) geq delta$, where $J(x) = frac12 (x + x^{-1}) - 1$.
background
The module establishes that J has a unique minimum at 1 and that continuous spaces permit infinitesimal perturbations with arbitrarily small defect, precluding stable minima. Discrete spaces enforce a finite step cost via the gap. Upstream, defect is defined by LawOfExistence.defect as equal to J for positive arguments. The structure packages configs, positivity, min_gap, and the isolation axiom gap_property.
proof idea
Structure definition that directly assembles the finite set, positivity constraints, positive gap size, and the forall statement encoding isolation of the unit point under defect.
why it matters
Supplies the type used by discrete_minimum_stable to conclude that the minimum at 1 is strictly isolated and by DiscreteLedger to witness finite step structure. It encodes the module's central step from continuous instability to discrete stability, aligning with J-uniqueness at T5 and the requirement for finite gaps to support RSExist.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.