DiscreteConfigSpace
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not construct an explicit finite set satisfying the gap_property.
- Does not prove that any such discrete space exists inside the Recognition framework.
- Does not relate min_gap to the second derivative J''(1) = 1.
- Does not extend the isolation argument to configuration spaces of dimension greater than one.
formal statement (Lean)
409structure DiscreteConfigSpace where
410 /-- The discrete configuration values -/
411 configs : Finset ℝ
412 /-- All configs are positive -/
413 configs_pos : ∀ x ∈ configs, 0 < x
414 /-- There's a minimum gap between adjacent configurations' J-costs -/
415 min_gap : ℝ
416 min_gap_pos : 0 < min_gap
417 /-- The gap property: any config x ≠ 1 has defect at least min_gap.
418 This ensures that 1 is strictly isolated as the unique minimum. -/
419 gap_property : ∀ x : ℝ, x ∈ configs → x ≠ 1 → defect x ≥ min_gap
420
421/-- **Key Theorem**: In a discrete configuration space, the unique minimum is stable.
422
423 If 1 ∈ configs (the point with defect = 0), then it's strictly isolated:
424 all other configurations have defect ≥ min_gap.
425
426 This is why discrete spaces support stable existence. -/