IsStable
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.