RSExists_stable
plain-language theorem explainer
RSExists_stable defines the predicate for a locked-in zero-defect configuration in the Recognition Science cost model. It holds precisely when defect(x) vanishes and x is isolated inside the given configuration space. Researchers proving that continuous spaces admit no stable points cite this predicate as the exact statement of stability. The definition is a direct conjunction of the zero-defect clause and the standard epsilon-isolation quantifier.
Claim. Let $Ssubseteqmathbb{R}$ be a configuration space. Then $mathrm{RSExists_stable}(x,S)$ holds if and only if $mathrm{defect}(x)=0$ and there exists $varepsilon>0$ such that for all $y in S$ with $yneq x$ one has $|y-x|>varepsilon$.
background
The DiscretenessForcing module shows how the J-cost landscape forces discrete structure. The defect functional equals J(x) = ½(x + x^{-1}) - 1 and therefore vanishes uniquely at x = 1. In logarithmic coordinates this becomes cosh(t) - 1, a strictly convex bowl centered at t = 0. Upstream, defect is imported from LawOfExistence as the direct identification defect(x) := J(x) for positive reals.
proof idea
This is a one-line definition. It conjoins the zero-defect condition supplied by LawOfExistence.defect with the standard metric isolation predicate on the configuration space Set ℝ.
why it matters
The predicate supplies the exact stability notion used by rs_exists_impossible_continuous and stable_existence_requires_discrete. Those theorems convert the definition into the claim that any stable point forces the configuration space to be discrete. In the Recognition Science chain this step links T5 J-uniqueness to the requirement of discrete steps (T7 eight-tick octave) because only a discrete lattice can isolate a point at the J-minimum. The module document states the key insight: continuous spaces allow infinitesimal perturbations of infinitesimal J-cost, so no configuration is locked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.