RSOutside
plain-language theorem explainer
A real configuration sits outside the stabilization classification when its defect neither vanishes nor exceeds every real bound. Classification theorems and the legacy Gödel-dissolution shim cite this residual case. The body is a pure conjunction of the two negations; once divergence is ruled out, it collapses to non-stabilizing.
Claim. For $c \in \mathbb{R}$, say $c$ is outside the stabilization classification when $\mathrm{defect}(c) \neq 0$ and it is not the case that $\forall C \in \mathbb{R},\, \mathrm{defect}(c) > C$.
background
The 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)$, plus corollaries on stabilization status. The phenomenon is propositional content (excluded middle on a predicate), not Recognition-Science-specific physics.
Stabilization means the defect vanishes: $\mathrm{defect}, c = 0$. Divergence means the defect exceeds every real bound: $\forall C,, \mathrm{defect}, c > C$. Defect itself comes from the Law of Existence layer (unique zero at $x=1$, strictly positive elsewhere).
The residual "outside" status is the conjunction of the two negations. A later lemma shows divergence is vacuous for any real-valued defect, so the residual reduces to non-stabilizing.
proof idea
Definitional, not a proof. The predicate is the conjunction $\neg(\mathrm{defect}, c = 0) \land \neg(\forall C,, \mathrm{defect}, c > C)$. No tactics or upstream lemmas are applied at the definition site; consumers discharge the second conjunct via the diverge-impossible lemma.
why it matters
Feeds the exhaustive split config_classification: every real $c$ either stabilizes or is outside. That theorem builds the outside witness as $\langle \neg\mathrm{stab},, \mathrm{diverge_impossible}, c \rangle$, so this definition is the residual case in the API. The same name is re-exported from the deprecated Gödel-dissolution shim for backward compatibility.
In the broader module arc it supports the claim that no real configuration is self-negating under defect-vanishing. The module doc is explicit that this does not touch Gödel I (Gödel sentences satisfy $G \leftrightarrow \neg\mathrm{Prov}_F(\ulcorner G\urcorner)$, a different biconditional). Framework landmarks T0–T8 are not invoked here; the content is pure classical logic on the defect predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.