SelfRefQuery
plain-language theorem explainer
SelfRefQuery packages a real number c with the biconditional that its defect vanishes if and only if it does not. Researchers working on the Gödel dissolution cite the structure to encode configurations that assert their own non-stabilization. The declaration is a plain structure definition with no lemmas or computational steps.
Claim. A self-referential stabilization query is a real number $c$ equipped with the property that defect$(c)=0$ holds if and only if it does not.
background
In this module defect is the functional J imported from LawOfExistence, so defect$(x)$ equals zero precisely when $x$ is a fixed point of the recognition dynamics. The sibling definition Stabilizes$(c)$ is therefore defect $c = 0$, i.e., iterated cost minimization converges. The module setting treats Gödel sentences as self-referential stabilization queries that assert their own non-membership in the ontology of cost-minimizing configurations.
proof idea
The declaration is a structure definition that directly encodes the contradictory biconditional on defect; no upstream lemmas are invoked and no tactics are applied.
why it matters
The structure supplies the contradictory object used by GodelDissolutionTheorem and complete_godel_dissolution to conclude that no such query exists, thereby reclassifying Gödel sentences as non-configurations rather than true-but-unprovable statements. It implements the paper's central claim that RS closure concerns unique cost minimizers, not arithmetic completeness, and aligns with the Recognition Composition Law by exposing an inconsistency inside the stabilization predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.