Diverges
plain-language theorem explainer
A real configuration c diverges when its defect function is unbounded above. Analysts of self-referential stabilization queries in the Gödel dissolution module cite this predicate to separate oscillating queries from stabilizing or diverging ones. The definition is introduced directly as a universal quantification over all real upper bounds C.
Claim. A configuration $c$ diverges if its defect satisfies $defect(c) > C$ for every real number $C$.
background
The module translates Gödel sentences into RS self-referential stabilization queries: configurations that encode the assertion 'I do not stabilize.' A query c is modeled so that its truth value equals the negation of its stabilization status. The defect function, drawn from the Cost module, quantifies deviation from the unique cost minimizer under the Recognition Composition Law.
proof idea
The declaration is a direct definition via universal quantification on the defect function; no lemmas or tactics are applied.
why it matters
This predicate supplies the diverging case in the trichotomy for self-referential queries, supporting the claim that such queries lie outside the ontology because they neither stabilize nor diverge. It feeds the dissolution argument that Gödel phenomena do not obstruct RS closure, which rests on cost minimization rather than arithmetic provability. The definition aligns with the eight-tick octave and phi-ladder structure by keeping defect comparisons inside RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.