stab_decidable
plain-language theorem explainer
Stabilization status of any real configuration is classically decidable: either its defect vanishes or it does not. Cited by the classical-logic half of the T0 bridge and by the unique-minimizer bundle. Proof is a one-line application of excluded middle to the vanishing-defect proposition.
Claim. For every real number $c$, either the defect of $c$ vanishes or it does not: $\mathrm{defect}(c)=0$ or $\mathrm{defect}(c)\neq 0$.
background
In this module a real configuration "stabilizes" precisely when its defect vanishes. The defect functional is the cost $J$: $\mathrm{defect}(x):=J(x)$. So the stabilization predicate is just $\mathrm{defect}(c)=0$.
The module proves classical-logic facts about real configurations: no configuration satisfies a self-negating biconditional $(\mathrm{defect},c=0)\leftrightarrow\neg(\mathrm{defect},c=0)$, and related corollaries about definite status and the unique zero-defect point at unity. The module doc is explicit that this is propositional content, not Gödel incompleteness: Gödel sentences satisfy $G\leftrightarrow\neg\mathrm{Prov}_F(\ulcorner G\urcorner)$, a different biconditional.
Upstream, defect comes from LawOfExistence and equals $J$ on positives; the present predicate is only a thin wrapper naming the zero set.
proof idea
One-line term proof. Apply classical excluded middle (em) directly to the proposition that the configuration stabilizes, i.e. to $\mathrm{defect}(c)=0$. No intermediate lemmas are required.
why it matters
Supplies the definite-status field of the bundled classical-logic-and-unique-minimizer theorem, and feeds the complete classical-logic-and-closure package (historically misnamed a Gödel dissolution; the content is ordinary classical logic plus unique existence at $x=1$).
In the forcing chain it is wired into t0_to_classical_logic_and_unique_minimizer_bridge_holds: under T0, the bridge records no self-negating configs, no general self-negating predicates, and definite stabilization status via this theorem. That is the classical-logic half of the T0 bridge; the substantive unique-minimizer half is the T5 $J$-uniqueness fact, not this lemma.
A compatibility re-export lives in the old GodelDissolution shim. The honest meta-level claim that Gödel I has no target inside T-1→T8 is outside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.