discrete_minimum_stable
plain-language theorem explainer
In a discrete configuration space containing the J-minimum at 1, every other configuration x satisfies defect(x) at least the minimum gap. Recognition Science modelers cite this to establish why discrete spaces permit stable existence while continuous ones do not. The proof is a one-line wrapper invoking the gap_property field of DiscreteConfigSpace.
Claim. Let $D$ be a discrete configuration space with $1$ among its positive real configurations. Then for every $x$ in those configurations with $x ≠ 1$, the defect of $x$ is at least the minimum gap of $D$.
background
DiscreteConfigSpace is the structure whose configs field is a Finset of positive reals, equipped with a positive min_gap and the gap_property ensuring that any x ≠ 1 has defect at least that gap. The module sets J(x) = ½(x + x⁻¹) - 1 with unique minimum at x = 1; in log coordinates this is cosh(t) - 1. RSExists requires defect = 0, which holds only at that point. Upstream, continuous_space_no_lockIn shows that in a connected continuous space any point with defect zero has nearby points with arbitrarily small defect, so no configuration is isolated.
proof idea
Term-mode proof. After intro x hx hx_ne the tactic applies the gap_property field of the supplied DiscreteConfigSpace instance D directly to the hypotheses.
why it matters
This result shows that the J-cost landscape permits stable minima once discreteness is imposed, completing the contrast drawn in the module with continuous_space_no_lockIn. It supplies one direction of the argument that RSExists forces a discrete configuration space (the other direction appears in the module's main theorems). It sits inside the T5 J-uniqueness step of the forcing chain and the cost-first existence development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.