diverge_impossible
plain-language theorem explainer
No real configuration can diverge in the strong sense that its defect exceeds every real bound: the defect is itself a real, so the claim is self-refuting. Anyone classifying stabilization status for real configurations cites this. The proof instantiates the universal bound at the defect value and obtains a strict self-inequality, discharged by linear arithmetic.
Claim. For every real configuration $c$, it is false that $\mathrm{defect}(c)$ exceeds every real number: $\neg(\forall C\in\mathbb{R},\,\mathrm{defect}(c)>C)$.
background
This module records classical facts about stabilization language for real configurations: no real $c$ can satisfy a biconditional of the form $(\mathrm{defect},c=0)\leftrightarrow\neg(\mathrm{defect},c=0)$, and related status predicates. The module doc is explicit that this is propositional-logic content, not a treatment of Gödel incompleteness.
A configuration is said to diverge when its defect exceeds every real bound: $\mathrm{RSDiverge}(c):\Leftrightarrow\forall C\in\mathbb{R},,\mathrm{defect}(c)>C$. The companion predicate "outside" means neither stabilizing nor diverging; the present theorem collapses that clause for real-valued defects. Defect itself is the real-valued cost/defect functional imported from the Law of Existence layer (zero only at the unique existent $x=1$).
The legacy GodelDissolution file re-exports the same statement under deprecated names; the canonical home is this module.
proof idea
Assume for contradiction that $c$ diverges, i.e. $\forall C,,\mathrm{defect}(c)>C$. Instantiate the quantifier at the real number $C=\mathrm{defect}(c)$ itself. The resulting hypothesis is $\mathrm{defect}(c)>\mathrm{defect}(c)$. Linear arithmetic (linarith) closes the contradiction. No external RS lemmas are required beyond the definition of divergence and the fact that defect is real-valued.
why it matters
This lemma is the content that makes the three-way status language honest for reals. Downstream, config_classification proves every real $c$ either stabilizes or is "outside"; the outside case is built as $\neg\mathrm{RSStab}\land\neg\mathrm{RSDiverge}$, and the second conjunct is discharged exactly by this theorem, so outside reduces to non-stabilizing. The legacy shim re-exports the same fact for older call sites.
In the broader Recognition foundation it is housekeeping, not a forcing-chain step (T0–T8). It clears a vacuous branch so later self-negation and unique-zero-defect arguments can speak only about stabilization versus failure to stabilize. The module deliberately does not claim a Lean dissolution of Gödel I; that remains a meta-level accounting outside this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.