no_self_negating_config
plain-language theorem explainer
No real configuration can satisfy the biconditional (defect equals zero) if and only if (defect is nonzero). Anyone citing classical closure of the Recognition existence predicate, or the unique zero-defect minimizer at unity, uses this fact. The proof is a two-line case split on excluded middle applied to the self-negation field of the configuration structure.
Claim. There is no real number $c$ together with a proof of $(\mathrm{defect}(c)=0)\leftrightarrow\neg(\mathrm{defect}(c)=0)$. Equivalently, the type of self-negating configurations is empty.
background
The module records a classical-logic triviality about Recognition configurations: no real $c$ can satisfy $P\leftrightarrow\neg P$ when $P$ is "defect vanishes." The defect functional is the Recognition cost $J$ on positive reals (from Law of Existence); zero defect marks the unique existent configuration at unity.
A self-negating configuration is a structure packing a real $c$ with a field asserting $(\mathrm{defect},c=0)\leftrightarrow\neg(\mathrm{defect},c=0)$. By classical logic that field is inhabited only if false. The module is explicit that this is propositional content, not Gödel self-reference: a Gödel sentence is $G\leftrightarrow\neg\mathrm{Prov}_F(\ulcorner G\urcorner)$, a consistent biconditional of a different shape.
Sibling material classifies stabilization status and packages the same fact for general predicates. Downstream bundles combine it with uniqueness of the zero-defect point $x=1$.
proof idea
Assume a self-negating configuration $q$ exists and unpack its self-negation biconditional $h$. Case-split on whether $\mathrm{defect}(q.\mathrm{config})=0$.
If the defect is zero, the forward direction of $h$ yields a contradiction with that same equality. If the defect is nonzero, the reverse direction of $h$ forces the defect to be zero, again a contradiction. Both branches discharge by excluded middle; no Recognition-specific lemmas are required beyond the structure fields.
why it matters
This is the atomic classical-logic brick for the module's bundled theorem ClassicalLogicAndUniqueMinimizerTheorem and for complete_classical_logic_and_closure (historically misnamed a "Gödel dissolution"). Those packages feed the unique RS-existent at $x=1$ and definite stabilization status for every real configuration.
It is re-exported under deprecated names in GodelDissolution for backward compatibility, with the honest disclaimer that it does not touch Gödel I. In the forcing chain it appears on the spine-to-extras bridge and in physical_forcing_chain packaging: classical nonexistence of $P\leftrightarrow\neg P$ configurations is part of the logical hygiene before T0–T8 force $J$, $\varphi$, the eight-tick octave, and $D=3$.
The open meta-question (why Gödel I has no target inside the RS forcing chain) remains outside Lean; this theorem only closes the propositional self-negation gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.