SelfNegatingConfig
plain-language theorem explainer
Packages a real number c with a witness that (defect c = 0) is equivalent to its own negation. Downstream theorems cite this type to state that no such pair exists under classical logic. Pure structure definition: two fields, no proof obligation beyond the Prop in the second field.
Claim. A self-negating configuration is a pair $(c, h)$ where $c \in \mathbb{R}$ and $h$ is a proof of $(\mathrm{defect}(c) = 0) \leftrightarrow \neg(\mathrm{defect}(c) = 0)$. Here $\mathrm{defect}$ is the RS defect functional (equal to the $J$-cost on positive reals).
background
The ambient module records the classical fact that no real configuration can satisfy a biconditional of the form $P \leftrightarrow \neg P$, specialized to stabilization. Stabilization means vanishing defect: a real $c$ stabilizes precisely when $\mathrm{defect}(c) = 0$. The defect functional is the RS cost $J$ on positive reals; at unity one has $\mathrm{defect}(1) = 0$, and elsewhere the defect is strictly positive when $x \neq 1$ in the relevant regime.
The module is explicit that this content is propositional logic, not Gödel incompleteness. A Gödel sentence has the shape $G \leftrightarrow \neg\mathrm{Prov}_F(\ulcorner G\urcorner)$, which is consistent; the structure here encodes the inconsistent $P \leftrightarrow \neg P$. Historical names such as SelfRefQuery in the compatibility shim are deprecated for that reason.
Upstream, defect comes from the Law of Existence layer; the stabilization predicate is the local abbreviation of vanishing defect.
proof idea
No proof body: this is a structure declaration. The first field is an underlying real configuration. The second field is the biconditional $(\mathrm{defect},c = 0) \leftrightarrow \neg(\mathrm{defect},c = 0)$, documented as inhabited if and only if False. Emptiness is discharged later by a two-line excluded-middle case split in the companion non-existence theorem, not here.
why it matters
This type is the carrier for the classical non-existence claim used throughout the foundation stack. The companion theorem proves there is no inhabitant; that fact is bundled into the classical-logic-and-unique-minimizer package and into the complete classical-logic-and-closure theorem (historically misnamed a Gödel dissolution). Downstream, the Unified Forcing Chain cites the same non-existence when stating classical negation impossibility alongside the unique minimizer, and the compatibility shim re-exports the structure under a deprecated self-reference name while warning that it is not a Gödel model.
In RS terms the point is narrow but load-bearing: every real configuration has definite stabilization status, so the forcing chain never has to entertain a configuration that both is and is not zero-defect. It does not touch T5–T8 (J-uniqueness, $\varphi$, eight-tick, $D=3$); those live elsewhere. The honest meta-level account of why Gödel I has no target inside the T-chain is outside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.