no_general_self_negating_predicate
plain-language theorem explainer
No real configuration admits a general predicate-level biconditional self-negation: there is no package of a real c, a proposition A, and proofs that A encodes non-stabilization while also agreeing with stabilization. Anyone citing the classical-logic half of the T0 bridge or the unique-minimizer bundle needs this. The proof collapses the two fields to P ↔ ¬P and splits on excluded middle.
Claim. There is no real number $c$, proposition $A$, and pair of equivalences $A \leftrightarrow \neg(\mathrm{defect}(c)=0)$ and $(\mathrm{defect}(c)=0) \leftrightarrow A$. Equivalently, no general predicate-level package realizing $(\mathrm{defect}(c)=0) \leftrightarrow \neg(\mathrm{defect}(c)=0)$ is inhabited.
background
Stabilization of a real configuration $c$ 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 module studies biconditional self-negation of that status: propositions of the schematic form $P \leftrightarrow \neg P$ with $P$ the stabilization predicate.
A general self-negating predicate packages a real config $c$, an auxiliary proposition $A$, a proof that $A$ encodes non-stabilization ($A \leftrightarrow \neg\mathrm{RSStab}(c)$), and a correctness link ($\mathrm{RSStab}(c) \leftrightarrow A$). Composing the two fields yields exactly $\mathrm{RSStab}(c) \leftrightarrow \neg\mathrm{RSStab}(c)$.
The module setting is classical propositional content, not RS-specific dynamics. As the module doc states: "The same fact holds for any predicate $P$: classical logic has no fixed point for negation." It explicitly does not address Gödel sentences of the form $G \leftrightarrow \neg\mathrm{Prov}_F(\ulcorner G\urcorner)$.
proof idea
Assume an inhabitant $q$ of the general self-negating structure. From its two field proofs (correctness and encodes-negation), transitivity of $\leftrightarrow$ produces $h : \mathrm{RSStab}(q.\mathrm{config}) \leftrightarrow \neg\mathrm{RSStab}(q.\mathrm{config})$.
Case-split on whether the config stabilizes. If it does, $h$ forward gives non-stabilization, contradiction. If it does not, $h$ backward gives stabilization from the negated hypothesis, again contradiction. Pure classical excluded-middle on a single proposition; no RS lemmas beyond the structure fields and the definition of stabilization.
why it matters
This is the general (predicate-level) half of the classical no-self-negation package. It is bundled into ClassicalLogicAndUniqueMinimizerTheorem alongside the config-level version, decidable stabilization status, and unique zero-defect existence at $x=1$.
In the forcing chain it feeds the T0 → classical-logic-and-unique-minimizer bridge: that bridge "bundles the classical-logic fact that $P \leftrightarrow \neg P$ has no inhabitant (in two formulations), excluded middle on the stabilization predicate, and the substantive T5 fact that the unique RS-existent is $x=1$." The holding theorem wires this result in directly, and the extended inevitability chain consumes the bridge.
Deprecated shims in the old Gödel-dissolution module re-export it under historical names. The honest framing is classical logic only; the categorical reason Gödel I has no target inside T-1→T8 is meta-level, not this Lean theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.