IsStable
A real number x is stable when it forms a strict local minimum of the defect functional. Researchers deriving discreteness from the Recognition Science cost landscape cite this definition when showing that continuous spaces admit no isolated minima. The definition encodes the neighborhood condition directly via the defect function.
claimA real number $x$ is stable if there exists $ε > 0$ such that for all real $y ≠ x$ with $|y - x| < ε$, the defect at $x$ is strictly less than the defect at $y$.
background
The Discreteness Forcing module shows that J(x) = ½(x + x^{-1}) - 1 has a unique minimum at x = 1, becoming cosh(t) - 1 in log coordinates. The upstream defect definition from LawOfExistence states: 'The defect functional. Equals J for positive x.' This identifies defect with J, so the cost landscape is a convex bowl with no flat regions except at the origin in log space.
proof idea
Direct definition of a strict local minimum for the defect function on the reals. No lemmas or tactics are applied; the body simply unfolds the neighborhood condition.
why it matters in Recognition Science
This definition supplies the precise notion of stability used by the IsStable declarations in LogicFromCost and PreLogicalCost, and by the stable_iff_boundary theorem. It fills the module's first main theorem that connected continuous spaces have no isolated J-minima, supporting the framework claim that continuous configuration spaces force all defects to collapse without locking.
scope and limits
- Does not prove existence of stable points in any space.
- Does not extend beyond one-dimensional real configurations.
- Does not embed continuity or path-connectedness into the definition.
- Does not address discrete or higher-dimensional cases.
formal statement (Lean)
313def IsStable (x : ℝ) : Prop :=
proof body
Definition body.
314 ∃ ε > 0, ∀ y : ℝ, y ≠ x → |y - x| < ε → defect x < defect y
315
316/-- In a path-connected space with continuous J, there are no isolated stable points.
317
318 Intuition: If x is stable with defect(x) = 0, and the space is path-connected,
319 we can find a path from x to any nearby point. Along this path, defect varies
320 continuously, so we can get arbitrarily close to zero defect at other points.
321
322 This prevents "locking in" to x — we can always drift away with negligible cost.
323
324 Note: The actual proof requires the intermediate value theorem and connectedness.
325 We use ℝ as the configuration space for concreteness. -/