IsStable
plain-language theorem explainer
IsStable defines a real number x as stable precisely when defect attains a strict local minimum there. Researchers tracing the cost-to-discreteness argument in Recognition Science cite it to separate continuous from discrete configuration spaces. The definition encodes the neighborhood condition directly from the defect functional.
Claim. A real number $x$ is stable if there exists $ε>0$ such that for all $y≠x$, $|y-x|<ε$ implies defect$(x)<$defect$(y)$.
background
The module DiscretenessForcing shows that continuous configuration spaces admit no isolated J-minima while discrete spaces permit them. Defect is the functional defect(x) := J(x) from LawOfExistence, where J(x) = ½(x + x^{-1}) - 1. Upstream results equate stability to zero cost in PreLogicalCost and LogicFromCost, and the module doc states that RS existence requires discrete configuration space.
proof idea
The declaration is the direct definition of a strict local minimum of the defect function on ℝ.
why it matters
This definition is referenced by IsStable in LogicFromCost and PreLogicalCost, which equate stability to zero cost. It supports the module's claim that continuous spaces have no stable minima while discrete spaces allow them, aligning with the forcing chain from cost to structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.