GeneralSelfNegatingPredicate
plain-language theorem explainer
Packages a real configuration together with a proposition that both equals and negates its stabilization status (defect zero). The four fields force P ↔ ¬P on the stabilization predicate, so the type is classically empty. Cited by the no-inhabitant theorems and by the T0 classical-logic bridge in the forcing chain. Definitional packaging only; emptiness is proved downstream.
Claim. A general self-negating predicate is a real configuration $c$ together with a proposition $A$ such that $A \leftrightarrow \neg(\mathrm{defect}(c)=0)$ and $(\mathrm{defect}(c)=0) \leftrightarrow A$. The two biconditionals compose to $(\mathrm{defect}(c)=0) \leftrightarrow \neg(\mathrm{defect}(c)=0)$.
background
The module establishes a classical-logic fact: no real configuration satisfies a biconditional of the form $P \leftrightarrow \neg P$ for the stabilization predicate. Stabilization means vanishing defect: $\mathrm{RSStab}(c)$ is defined as $\mathrm{defect}(c)=0$, and defect is the cost functional $J$ (equal to $J$ on positive reals). The unique zero of defect is at $x=1$ by the law of existence.
This structure is the general, predicate-level packaging of that contradiction. It pairs a real $c$ with an arbitrary proposition $A$ that is required both to equal and to negate stabilization of $c$. The module is explicit that this is propositional logic content, not a model of a Gödel sentence: Gödel sentences satisfy $G \leftrightarrow \neg\mathrm{Prov}_F(\ulcorner G\urcorner)$, a consistent biconditional between distinct propositions.
Upstream, defect comes from LawOfExistence; RSStab is the local alias for defect-zero. The historical GodelDissolution module re-exports this structure under a deprecated name.
proof idea
No proof body: this is a structure definition. The four fields are data. Inhabitation would require a real $c$ and a proposition $A$ with both $A \leftrightarrow \neg\mathrm{RSStab}(c)$ and $\mathrm{RSStab}(c) \leftrightarrow A$. Transitivity of $\leftrightarrow$ immediately yields $\mathrm{RSStab}(c) \leftrightarrow \neg\mathrm{RSStab}(c)$, which is discharged as False by excluded middle in the downstream theorem no_general_self_negating_predicate.
why it matters
This is the general form of biconditional self-negation used throughout the foundation layer. Downstream, no_general_self_negating_predicate proves the type is empty, and ClassicalLogicAndUniqueMinimizerTheorem bundles that emptiness with the unique-minimizer fact at $x=1$. The same emptiness is a field of T0_To_ClassicalLogicAndUniqueMinimizer_Bridge in UnifiedForcingChain, feeding ultimate_inevitability_extended.
In the forcing chain it sits at the T0 classical-logic step: before J-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8). The module and the bridge doc-comments both warn that this does not refute Gödel I; it only records that $P \leftrightarrow \neg P$ has no inhabitant. The honest meta-level accounting lives outside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.