ClassicalLogicAndUniqueMinimizerTheorem
plain-language theorem explainer
Bundle of four claims: no real configuration satisfies defect-zero biconditional self-negation; none carries a general stabilization self-negation P↔¬P; every real has definite stabilization status; and RS existence picks a unique real. Foundation readers cite it as the classical-logic-plus-unique-minimizer package on the T0 bridge. As a structure it only declares the interface; the inhabitant is assembled field-wise from sibling lemmas.
Claim. A record packaging four assertions: (i) there is no real configuration $c$ with $(\mathrm{defect}(c)=0)\leftrightarrow\neg(\mathrm{defect}(c)=0)$; (ii) there is no real carrying a general biconditional self-negation of stabilization status; (iii) for every real $c$, either the defect vanishes or it does not; (iv) there exists a unique real $x$ that is an RS-existent.
background
Stabilization means the defect of a real configuration vanishes: $\mathrm{RSStab},c$ is defined as $\mathrm{defect}(c)=0$. A self-negating configuration pairs a real with the biconditional $(\mathrm{defect}=0)\leftrightarrow\neg(\mathrm{defect}=0)$. A general self-negating predicate encodes $\mathrm{RSStab},c\leftrightarrow A\leftrightarrow\neg\mathrm{RSStab},c$, which collapses to $P\leftrightarrow\neg P$.
The module setting is classical propositional content on real configurations: no inhabitant of $P\leftrightarrow\neg P$, plus definite status and the unique zero-defect existent. The module doc is explicit that this is not Gödel incompleteness. Gödel sentences satisfy $G\leftrightarrow\neg\mathrm{Prov}_F(\ulcorner G\urcorner)$, a different and consistent shape.
Upstream, emptiness of the two self-negation structures is already proved by excluded-middle case split and by transitivity of $\leftrightarrow$ on the general predicate fields.
proof idea
Structure declaration only: no proof body. It names four fields whose types are the classical no-self-negation facts, excluded middle on stabilization, and unique RS existence. The inhabitant is built downstream by assigning the sibling theorems no_self_negating_config, no_general_self_negating_predicate, stab_decidable, and rs_exists_unique to those fields.
why it matters
Supplies the type for the T0-to-classical-logic-and-unique-minimizer bridge in the unified forcing chain, which packages these facts after T0 (logic forced). The companion theorem constructs the unique inhabitant of this structure. Deprecated Gödel-dissolution aliases point here; the module renames away from that framing because the content does not touch incompleteness. The first three fields are classical logic; the fourth is the substantive RS claim of a unique existent (defect zero at the identity). Landmark placement: logic end of the T0–T8 chain, before J-uniqueness (T5) and $\varphi$ (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.