RSDiverge
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.