DiscreteConfigSpace
plain-language theorem explainer
DiscreteConfigSpace encodes a finite set of positive reals whose J-defects are separated by a positive minimum gap. Researchers modeling stable minima in Recognition Science cost landscapes cite this structure to formalize isolation of the unit configuration. The definition directly records the gap_property axiom ensuring no other config can approach defect zero.
Claim. A finite set $S$ of positive reals equipped with a positive real number $δ > 0$ such that $J(x) ≥ δ$ for every $x ∈ S$ with $x ≠ 1$, where $J(x) = ½(x + x^{-1}) - 1$ is the defect functional.
background
The DiscretenessForcing module shows that stable configurations require discrete steps in the J-cost landscape. J(x) = ½(x + x^{-1}) - 1 has a unique minimum at x = 1; in log coordinates this is cosh(t) - 1, a convex bowl. Continuous spaces permit infinitesimal perturbations with arbitrarily small cost, so no configuration is locked in. Discrete spaces enforce a finite step cost, allowing minima to be trapped.
proof idea
This is a direct structure definition. The fields configs, configs_pos, min_gap, min_gap_pos and gap_property are recorded as axioms with no lemmas applied and no computational reduction.
why it matters
The structure supplies the hypothesis for discrete_minimum_stable, which concludes that the unit configuration is strictly isolated when present. It is also used in DiscreteLedger to witness finite step structure inside PhiForcing. The definition fills the module's claim that RS existence requires a discrete configuration space, closing the step from continuous drift to trapped minima in the cost-to-structure forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.