rs_exists_impossible_continuous
plain-language theorem explainer
Stable existence at the J-minimum cannot hold in any connected dense subset of the reals containing 1. Researchers deriving discreteness from the Recognition Science cost landscape would cite this to exclude continuous configuration spaces. The term proof assumes an isolating neighborhood around 1 and invokes the density hypothesis to produce a nearby point inside it, with linear arithmetic closing the contradiction.
Claim. Let $Ssubseteqmathbb{R}$ contain $1$ and be connected with no isolated points. Then the predicate requiring defect$(1)=0$ together with an isolating radius around $1$ in $S$ is false.
background
The Discreteness Forcing module bridges the J-cost landscape to structural discreteness. J$(x)=frac12(x+x^{-1})-1$ has a unique minimum of zero at $x=1$; in logarithmic coordinates this is $cosh(t)-1$, a convex bowl. The stable existence predicate requires both zero defect and isolation: defect$(x)=0$ and existence of $varepsilon>0$ such that every other point of the space lies outside the $varepsilon$-ball. Upstream, defect is defined as J in the LawOfExistence module, and the density hypothesis directly negates isolation.
proof idea
The term-mode proof introduces the assumption of stable existence at 1 to obtain an isolating $varepsilon$. The density hypothesis supplies a distinct $y$ in the space with $|y-1|<varepsilon$, violating isolation. Linear arithmetic on the distance inequalities yields the contradiction.
why it matters
The result formalizes the forcing of discreteness by the J-cost landscape and occupies the position of continuous_no_stable_minima in the module. It supplies the step from J-uniqueness (T5) to the necessity of discrete steps for stability in the T0-T8 chain. The module positions it as the key lemma showing that RSExists implies a discrete configuration space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.