RSOutside
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assert existence of any RSOutside configuration.
- Does not constrain the value of defect for such c.
- Does not link to concrete physical models or the phi-ladder.
formal statement (Lean)
119def RSOutside (c : ℝ) : Prop := ¬RSStab c ∧ ¬RSDiverge c
proof body
Definition body.
120
121/-- A more general self-referential query: c encodes "I don't RSStab."
122 We model this as: there's a function φ that tells us "what c asserts"
123 and c asserts ¬RSStab(c). -/