stable_existence_requires_discrete
plain-language theorem explainer
The theorem states that if a stable recognition configuration exists in some space, then a discrete configuration space supporting an isolated zero-defect point must exist. Researchers tracing the Recognition Science forcing chain from cost axioms to spatial structure would cite this as the logical bridge between RS existence and topological discreteness. The proof is a one-line term wrapper that reorders the existential quantifiers after introducing the witness pair from the stable predicate.
Claim. If there exists a real number $x$ and a subset $Csubseteqmathbb{R}$ such that the defect of $x$ is zero and $x$ is isolated in $C$, then there exists a subset $Csubseteqmathbb{R}$ and a real number $x$ satisfying the same isolation and zero-defect conditions.
background
The Discreteness Forcing module centers on the cost functional $J(x)=frac12(x+x^{-1})-1$, which becomes $cosh(t)-1$ in log coordinates and has a unique minimum at $x=1$. The predicate RSExists_stable$(x,C)$ holds when defect$(x)=0$ and there is $varepsilon>0$ such that every other point in $C$ lies at least $varepsilon$ away from $x$. The module argument is that continuous spaces permit infinitesimal perturbations of vanishing $J$-cost, so no point can be isolated, while discrete spaces enforce finite step costs that trap configurations at the minimum.
proof idea
The term proof introduces the witness pair via intro $langle x, config_space, hstable rangle$ and immediately returns the reordered triple $langle config_space, x, hstable rangle$. It is a one-line wrapper that applies the commutativity of nested existential quantifiers to the stable-existence hypothesis.
why it matters
This corollary supplies the formal statement that stable existence (defined via zero defect and isolation) requires a discrete configuration space, directly implementing the Level 2 step of the forcing chain: Composition law to unique $J$-minimum to discreteness. It sits between the RSExists predicate from CostFirstExistence and the module summary that lists the progression Composition law → J unique → Discreteness forced → Ledger → phi → D=3. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.