GeneralSelfRefQuery
plain-language theorem explainer
GeneralSelfRefQuery defines a structure pairing a real configuration c with a proposition P that encodes the negation of c's own RS stabilization while also requiring that stabilization status to match P exactly. Logicians and physicists studying whether incompleteness results block unique cost-minimizing closures would cite this definition. It is introduced as a pure structure definition with no proof obligations.
Claim. A structure consisting of a real number $c$ and a proposition $P$ such that $P$ is equivalent to the negation of the stabilization predicate on $c$, and the stabilization predicate on $c$ is equivalent to $P$, where the stabilization predicate holds precisely when the defect of $c$ is zero.
background
RSStab(c) is the predicate defect(c) = 0 that marks stabilization (RS-truth) in the cost model. The module formalizes self-referential stabilization queries as configurations that assert their own non-stabilization, showing they lie outside the ontology rather than being true-but-unprovable. This setting rests on the upstream distinction between formal proof systems and selection by cost minimization, with RSStab imported directly from the same module's sibling definition.
proof idea
This is a structure definition that introduces four fields: config of type real, asserts of type Prop, encodes_negation witnessing the biconditional with negation of stabilization, and correctness witnessing the biconditional with stabilization itself.
why it matters
The structure supplies the hypothesis for the downstream theorem general_self_ref_impossible, which derives a contradiction from the two biconditionals, and for GodelDissolutionTheorem, which concludes that self-referential queries are non-configurations. It thereby supports the paper claim that Gödel phenomena do not obstruct RS closure, because closure requires only a unique cost minimizer rather than arithmetic completeness. The construction aligns with the framework's T0-T8 forcing chain by keeping the ontology limited to cost-minimizing fixed points.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.