stab_decidable
plain-language theorem explainer
Any real configuration in Recognition Science has a definite stabilization status: its defect is either zero or nonzero. Researchers formalizing the Gödel dissolution would cite this to exclude indeterminate states for self-referential queries. The proof is a one-line application of the law of excluded middle to the RSStab predicate.
Claim. For every real number $c$, either defect$(c)=0$ or defect$(c)≠0$.
background
The module formalizes the claim that self-referential stabilization queries have no fixed point under RS dynamics and therefore lie outside the ontology. Defect is the functional J(x) from LawOfExistence, with RSStab defined as defect c = 0 and RSDiverge as the statement that defect c exceeds every real. The local setting treats Gödel sentences as translated into stabilization queries that assert their own non-stabilization.
proof idea
One-line wrapper that applies the excluded-middle principle directly to the proposition RSStab c.
why it matters
This supplies the definite_status field inside godel_dissolution_holds, which in turn feeds complete_godel_dissolution. The parent result uses it to conclude that self-referential queries are non-configurations rather than true-but-unprovable, thereby separating RS closure (unique cost minimizer) from arithmetic completeness. It closes the ontological gap required by the module's main theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.