RSOutside
plain-language theorem explainer
RSOutside classifies a real number c as outside the RS ontology when it satisfies neither the stabilization predicate nor the divergence predicate. Researchers citing the cost-theoretic dissolution of Gödel's theorem reference this definition to reclassify self-referential queries as non-configurations. The definition is introduced directly as the conjunction of the two negations.
Claim. A real number $c$ lies outside the ontology when defect$(c) ≠ 0$ and it is not the case that defect$(c)$ exceeds every real number.
background
The Gödel Dissolution module formalizes self-referential stabilization queries as configurations asserting they do not stabilize. RSStab c holds precisely when defect c equals zero. RSDiverge c holds when defect c exceeds every real bound. The local setting treats RS dynamics as cost minimization over real configurations, with stabilization and divergence as the only two truth-apt outcomes.
proof idea
This is a direct definition that conjoins the negations of RSStab and RSDiverge.
why it matters
RSOutside supplies the third classification used by config_classification to prove every real configuration is either RSStab or RSOutside. It implements the module's claim that Gödel sentences become non-configurations rather than true-but-unprovable statements. The definition closes the trichotomy needed for the paper's resolution that RS closure concerns unique cost minimizers, not arithmetic provability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.