RSDiverge
plain-language theorem explainer
A real configuration diverges when its defect is unbounded above: larger than every real threshold. The predicate is the negative pole of the stabilize/diverge classification used in the biconditional self-negation module. It is pure definitional packaging of the defect functional; no proof content. Downstream, it is immediately shown empty for every real input.
Claim. For a real configuration $c$, say that $c$ diverges when $\mathrm{defect}(c) > C$ for every real bound $C$. Equivalently, the defect is unbounded above.
background
The ambient module establishes 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 module is explicit that this is propositional content, not a treatment of Gödel incompleteness.
The defect functional is the Recognition cost on configurations: $\mathrm{defect}(x)=J(x)$ for the standard $J$-cost (and equals zero only at unity). Stabilization means zero defect. Divergence is defined here as the opposite extreme: defect larger than every real bound.
Together with the stabilize predicate, this supplies the two labels used by the outside-classification predicate and by the theorem that divergence never occurs for real-valued defect.
proof idea
Definitional, not a theorem. The body is the universal quantification $\forall C:\mathbb{R},,\mathrm{defect},c>C$. No tactics or lemmas are applied at the definition site; the mathematical work sits in the companion theorem that this predicate is uninhabited for every real $c$ (instantiate the bound at the defect itself and obtain a strict self-inequality).
why it matters
Gives the negative half of the stabilize/diverge vocabulary for real configurations. Immediate consumers are the emptiness theorem for divergence and the outside-classification predicate (neither stabilizes nor diverges), which collapses to non-stabilization once divergence is ruled out. The same name is re-exported from the backward-compatibility shim that formerly carried the misleading Gödel-dissolution label.
In the broader foundation stack this is bookkeeping around the Law of Existence defect, not a forcing-chain step (T5–T8). It keeps the stabilize/diverge language honest: for real defect there is no third “runaway” status, only zero versus positive cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.