RSDiverge
RSDiverge(c) defines the divergence predicate for a real configuration c as the claim that its defect exceeds every real bound C. It is cited in the Gödel dissolution argument to show self-referential stabilization queries cannot be RS-false. The definition is a direct universal quantification over the imported defect functional.
claimFor a configuration $c$ in the reals, RSDiverge$(c)$ holds precisely when the defect of $c$ is unbounded above: $∀ C ∈ ℝ, defect(c) > C$.
background
The Gödel Dissolution module translates self-reference into cost-minimization queries under Recognition Science dynamics. Defect is the functional imported from LawOfExistence, defined as defect(x) := J(x) and satisfying defect(1) = 0. RSDiverge pairs with the stabilization predicate RSStab (defect = 0) to partition configurations inside the ontology.
proof idea
One-line definition that directly applies the defect functional: RSDiverge(c) is the proposition ∀ C, defect c > C. No lemmas or tactics are invoked beyond the upstream defect definition.
why it matters in Recognition Science
RSDiverge supplies the RS-falsity side of the ontology partition, feeding diverge_impossible (which proves the predicate is empty for real c) and RSOutside (neither stab nor diverge). It completes the cost-theoretic step showing self-referential queries have no fixed point and lie outside the ontology, consistent with the module's resolution that Gödel phenomena do not obstruct RS closure.
scope and limits
- Does not claim any real configuration satisfies RSDiverge.
- Does not extend the predicate to non-real or non-configuration domains.
- Does not provide a constructive witness or example of divergence.
Lean usage
theorem test (c : ℝ) : ¬RSDiverge c := by intro h; have : defect c > defect c := h (defect c); linarithformal statement (Lean)
116def RSDiverge (c : ℝ) : Prop := ∀ C : ℝ, defect c > C
proof body
Definition body.
117
118/-- Outside the ontology: neither stabilizes nor diverges. -/