continuous_space_no_lockIn
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.
claimSuppose $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 in Recognition Science
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.
scope and limits
- Does not establish existence of stable points in any space.
- Does not bound the defect of nearby points.
- Does not apply to discrete configuration spaces.
- Does not quantify the minimum gap.
formal statement (Lean)
391theorem continuous_space_no_lockIn (x : ℝ) (hx_pos : 0 < x) (hx_exists : defect x = 0) :
392 ∀ ε > 0, ∃ y : ℝ, y ≠ x ∧ |y - x| < ε := by
proof body
Term-mode proof.
393 intro ε hε
394 have hx_eq_one : x = 1 := (defect_zero_iff_one hx_pos).mp hx_exists
395 subst hx_eq_one
396 -- Any nearby point exists
397 use 1 + ε / 2
398 constructor
399 · linarith
400 · simp only [add_sub_cancel_left, abs_of_pos (by linarith : ε / 2 > 0)]
401 linarith
402
403/-! ## Stability in Discrete Spaces -/
404
405/-- A discrete configuration space with finite step cost.
406
407 In a discrete space, adjacent configurations are separated by a minimum
408 "gap" in J-cost. This allows configurations to be "trapped" at minima. -/