continuous_space_no_lockIn
plain-language theorem explainer
Continuous configuration spaces admit no isolated zero-defect points. Given x > 0 with defect(x) = 0, every neighborhood contains another point y. Arguments showing why stable existence requires discreteness cite this result. The term proof first invokes the zero-defect characterization to fix x at 1, then exhibits an explicit nearby point.
Claim. Suppose $x > 0$ satisfies $J(x) = 0$. Then for every $ε > 0$ there exists $y ≠ x$ such that $|y - x| < ε$.
background
The defect functional equals the J-cost, defined as $J(x) = ½(x + x^{-1}) - 1$ for positive x. This function has a unique minimum of zero at x = 1, as established by the characterization theorem defect_zero_iff_one. The module DiscretenessForcing shows that continuous spaces allow infinitesimal perturbations with arbitrarily small cost, preventing lock-in at minima. Upstream results include the step function from cellular automata and the active edge count A.
proof idea
The term proof begins by applying defect_zero_iff_one to the hypothesis defect x = 0 and x > 0, yielding x = 1. It then substitutes and constructs y = 1 + ε/2, verifying y ≠ 1 by linarith and the distance bound by simplification and linarith.
why it matters
This theorem establishes that continuous spaces lack isolated minima, directly supporting the claim that discreteness is required for stable existence. It feeds the downstream result discrete_minimum_stable, which proves the unique minimum is isolated in discrete spaces. The argument aligns with the Recognition Science forcing chain, where J-uniqueness at T5 and the convex bowl in log coordinates imply that only discrete steps can trap configurations at the phi-ladder minimum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Tiny changes fool neural networks and transfer across models
"we find that there is no distinction between individual high level units and random linear combinations of high level units, according to various methods of unit analysis. It suggests that it is the space, rather than the individual units, that contains the semantic information in the high layers of neural networks."