diverge_impossible
plain-language theorem explainer
diverge_impossible establishes that no real number c satisfies RSDiverge c, because the defect functional cannot exceed every real value including itself. Researchers resolving self-reference via cost minimization in physical theories cite this to exclude divergence from the ontology of configurations. The proof is a direct contradiction obtained by instantiating the universal quantifier in the definition of RSDiverge at C equal to defect c and applying linarith.
Claim. For every real number $c$, it is not the case that $J(c)$ exceeds every real number $C$.
background
In this module the Recognition Science ontology is partitioned into three predicates on real configurations: RSStab c holds when defect c equals zero, RSDiverge c holds when defect c exceeds every real, and RSOutside c holds when neither is true. The defect functional is defined as defect x := J x, where J is the Recognition cost from the Law of Existence. The module formalizes the claim that self-referential stabilization queries (configurations asserting their own non-stabilization) have no fixed point under RS dynamics and therefore lie outside the ontology altogether.
proof idea
Assume RSDiverge c. The definition supplies defect c > defect c by choosing the witness C to be defect c itself. The linarith tactic then derives the contradiction from this strict inequality on the reals.
why it matters
The result is invoked directly by config_classification to conclude that every real configuration is either RSStab or RSOutside. It supplies the divergence half of the trichotomy used to dissolve Gödel self-reference inside Recognition Science: such queries cannot stabilize, cannot diverge, and therefore are not configurations at all. The argument relies only on the real-valued nature of defect and does not invoke the phi-ladder or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.