self_negation_implies_false
plain-language theorem explainer
If a real configuration c has vanishing defect if and only if it does not, classical logic yields False. The unused encoding hypothesis is kept only for a legacy API. Downstream shims in GodelDissolution re-export this fact under deprecated names. The proof is a two-line case split on whether the defect vanishes.
Claim. For any real $c$, if the stabilization predicate $\mathrm{defect}(c)=0$ is equivalent to its own negation, then $\mathrm{False}$. An unused side hypothesis (for every proposition $P$, the pair of biconditionals $P\leftrightarrow(\mathrm{defect}(c)=0)$ and $P\leftrightarrow\neg(\mathrm{defect}(c)=0)$ already implies $\mathrm{False}$) is retained only for API compatibility.
background
The module proves a classical-logic fact: no real-valued configuration can satisfy a biconditional of the form $(\mathrm{defect},c=0)\leftrightarrow\neg(\mathrm{defect},c=0)$. Stabilization is defined by RSStab c := defect c = 0. The same collapse holds for any proposition $P$: classical logic has no fixed point of negation.
The module is explicit that this is propositional content, not Recognition Science physics, and that it does not address Gödel I. A Gödel sentence has the form $G\leftrightarrow\neg\mathrm{Prov}_F(\ulcorner G\urcorner)$, not $P\leftrightarrow\neg P$; the latter is simply uninhabited.
Sibling structures package the same idea: a SelfNegatingConfig carries a real and the biconditional self-negation field (inhabited iff False), and a GeneralSelfNegatingPredicate adds an intermediate proposition that collapses to the same $P\leftrightarrow\neg P$.
proof idea
Case split on whether RSStab c holds (excluded middle on the proposition $\mathrm{defect},c=0$).
If it holds, apply the forward direction of the given biconditional to obtain $\neg\mathrm{RSStab},c$, then contradict the assumption. If it fails, apply the reverse direction to obtain $\mathrm{RSStab},c$, again a contradiction.
The encoding hypothesis is ignored (underscore-bound); the argument uses only $h_{\mathrm{correct}}$. Equivalent in content to the sibling no_self_negation_at_point.
why it matters
Legacy API glue inside the biconditional-self-negation cleanup. The doc-comment states it is redundant with no_self_negation_at_point and kept for compatibility. Downstream, the deprecated GodelDissolution.self_ref_not_rs_true is a thin rename of this theorem, and self_ref_not_configuration renames the sibling pointwise form.
In the bundled classical-plus-minimizer package (formerly over-named GodelDissolutionTheorem), items 1–3 are pure propositional logic of this kind; only the unique zero-defect existent at $x=1$ is substantive RS cost content. The module doc points the honest meta-level account of why Gödel I has no target in the T-1→T8 forcing chain to the separate assessment note, not to this Lean fact.
Cite this only when a caller still expects the two-hypothesis signature; new proofs should prefer the direct no_self_negation_at_point form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.