config_classification
plain-language theorem explainer
Every real configuration either has vanishing defect or sits outside the stabilization class. Workers on the Law of Existence and the self-negation corollaries cite this dichotomy as the exhaustive status split. The proof is a classical case split on stabilization; the outside branch is filled by the impossibility of real-valued divergence, so the second disjunct adds no new content beyond non-stabilization.
Claim. For every real number $c$, either the defect of $c$ vanishes, or $c$ neither stabilizes nor diverges. Equivalently: every real configuration either stabilizes ($\mathrm{defect}(c)=0$) or fails to stabilize, since divergence (defect exceeding every real bound) is impossible for real-valued defect.
background
This module records the classical-logic fact that no real configuration can satisfy a biconditional of the form $(\mathrm{defect},c=0)\leftrightarrow\neg(\mathrm{defect},c=0)$, plus a few status corollaries. Stabilization means vanishing defect: a real $c$ stabilizes precisely when $\mathrm{defect},c=0$. Divergence would mean the defect exceeds every real bound. Outside status is the conjunction of non-stabilization and non-divergence.
Upstream, diverge_impossible shows divergence is vacuous for any real-valued defect: take the bound equal to the defect itself and obtain a strict self-inequality. Consequently the outside predicate collapses to plain non-stabilization on $\mathbb{R}$. The module is explicit that this content is propositional logic, not a model of Gödel self-reference.
Cross-references in the module point to the Law of Existence facts that defect vanishes at $x=1$ and is positive elsewhere, which fix the unique zero-defect existent once the status split is in hand.
proof idea
Classical case split on whether $c$ stabilizes. If it does, take the left disjunct. If not, package the negation together with diverge_impossible c (which supplies $\neg$ diverge) to inhabit the outside predicate, and take the right disjunct. No further arithmetic on defect is required; the only lemma used is the vacuity of real-valued divergence.
why it matters
The theorem is the exhaustive status split for real configurations in the biconditional-self-negation development. Downstream it is re-exported verbatim under the legacy GodelDissolution namespace (same statement, deprecated home), and the sibling diverge_impossible is re-exported alongside it. Those shims keep older call sites compiling while the canonical home is this module.
Inside the module the classification feeds the structures that encode a configuration claiming $(\mathrm{defect},c=0)\leftrightarrow\neg(\mathrm{defect},c=0)$ and the theorems that no such inhabitant exists. The module doc is emphatic: this does not address Gödel I; a Gödel sentence is $G\leftrightarrow\neg\mathrm{Prov}_F(\ulcorner G\urcorner)$, a consistent biconditional of a different shape. The categorical claim that Gödel I has no target inside the RS forcing chain (T-1 through T8 to constants) remains meta-level, not a Lean theorem.
For the Recognition framework the payoff is local hygiene: every real configuration is either the unique zero-defect point or strictly positive defect, with no third "divergent" bucket on $\mathbb{R}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.