RSStab
plain-language theorem explainer
Stabilization of a real configuration c means its defect vanishes: defect(c) = 0. Anyone working the classical-logic closure or unique-minimizer bundle cites this predicate as the positive half of the stabilize/outside dichotomy. It is a one-line definitional alias of the Law of Existence defect functional.
Claim. A real configuration $c \in \mathbb{R}$ is said to stabilize when its defect vanishes: $\mathrm{defect}(c) = 0$. (Equivalently, since defect equals the $J$-cost on positives, $J(c) = 0$ when $c > 0$.)
background
The ambient module proves a classical-logic fact: no real configuration can satisfy a biconditional of the form $(\mathrm{defect}, c = 0) \leftrightarrow \neg(\mathrm{defect}, c = 0)$, together with corollaries on stabilization status and the unique zero-defect existent at $x = 1$. The module is explicit that this is propositional content (excluded middle on $P \leftrightarrow \neg P$), not a Gödel incompleteness argument.
The defect functional is defined in Law of Existence as $\mathrm{defect}(x) := J(x)$, the Recognition cost. Upstream facts record $\mathrm{defect}(1) = 0$ and $\mathrm{defect}(x) > 0$ for $x \neq 1$. Stabilization is simply the zero set of that functional, phrased as a named proposition so downstream structures can talk about stabilize vs. outside without repeating the equation.
Sibling predicates in the same file include divergence (defect unbounded) and "outside" (neither stabilizes nor diverges). Divergence is later shown impossible for real $c$, so the classification collapses to stabilize or not.
proof idea
Definitional. The body is the proposition $\mathrm{defect}, c = 0$; there is no proof obligation. Downstream theorems treat membership in this predicate by unfolding or by cases on excluded middle (by_cases hs : RSStab c).
why it matters
This predicate is the positive atom of the module's classification and self-negation apparatus. It appears in config_classification (every real is stabilize or outside), in the structures SelfNegatingConfig and GeneralSelfNegatingPredicate (which encode $P \leftrightarrow \neg P$ with $P =$ stabilize), and in the impossibility theorems no_self_negating_config, no_general_self_negating_predicate, and self_negation_implies_false.
Those facts are bundled into ClassicalLogicAndUniqueMinimizerTheorem and the complete closure theorem (historically misnamed a "Gödel dissolution"; the content is classical logic plus the unique existent at unity). In the Recognition forcing picture this sits under Law of Existence and the unique zero of $J$ at $x = 1$, not under T5–T8 themselves. It does not touch incompleteness; the module doc points meta-level Gödel discussion elsewhere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.