T0_To_ClassicalLogicAndUniqueMinimizer_Bridge
plain-language theorem explainer
Bridge certificate from T0 (logic forced by cost) packing classical impossibility of biconditional self-negation, excluded middle on stabilization, and the unique RS-existent at x=1. Downstream CompleteForcingChain and the holds theorem cite it. It is a Prop-structure of named classical and T5 facts, not a Gödel refutation; certificates are propositionally unique via Subsingleton.
Claim. Given a witness that logic is forced from recognition cost (consistent floor cost zero, inconsistent floor cost positive), the bridge asserts: no configuration satisfies $P\leftrightarrow\neg P$ (in config and general-predicate forms); every real $c$ has definite stabilization status $\mathrm{RSStab}(c)\lor\neg\mathrm{RSStab}(c)$; there is a unique real $x$ with $\mathrm{RSExists}(x)$, and $\mathrm{RSExists}(x)\leftrightarrow x=1$; the bundled classical-logic-and-unique-minimizer theorem holds; and the four-way conjunction of no self-negating config, unique existent, existent-iff-one, and definite stab status holds.
background
In the Unified Forcing Chain, T0 states that logic is not pre-given: at the pre-analytic floor it is the zero/positive split of recognition work (consistent configurations cost zero, inconsistent ones cost positive). The module aims to force the full T-1 through T8 ladder from the Recognition Composition Law plus normalization and calibration.
Upstream, ClassicalLogicAndUniqueMinimizerTheorem bundles the same classical facts: no real configuration satisfies $(\mathrm{defect}=0)\leftrightarrow\neg(\mathrm{defect}=0)$, no general biconditional self-negation, and definite stabilization status. A general self-negating predicate encodes $\mathrm{RSStab},c\leftrightarrow\mathrm{asserts}\leftrightarrow\neg\mathrm{RSStab},c$, which collapses to $P\leftrightarrow\neg P$ and has no inhabitant.
The unique-minimizer side is the substantive T5 content: the RS-existent (closure meaning: unique $J$-minimizer) is exactly $x=1$. The historical name claimed "Gödel dissolution"; the doc-comment explicitly renounces that reading.
proof idea
This declaration is a Prop-valued structure (a certificate type), not a proved theorem. Its fields are named hypotheses to be filled by the companion holds theorem.
That holds theorem is a field-by-field constructor: it assigns no_self_negating_config and no_general_self_negating_predicate from the corresponding BiconditionalSelfNegation lemmas, definite_stab_status from stab decidability (excluded middle on the stabilization predicate), and the unique-existent / existent-iff-one / bundled theorem fields from the same classical-plus-T5 package. A Subsingleton instance shows any two certificates for fixed T0 are definitionally equal (allEq by rfl).
why it matters
The bridge is a named link in the Complete Inevitability Chain: CompleteForcingChain consumes T0-level bridges so that every rung T0–T8 is recorded as forced from cost, not merely compatible. The honest rename from the deprecated Gödel-dissolution alias matters for the framework claim: what is forced here is classical biconditional impossibility plus the T5 unique $J$-minimizer at $x=1$, not a refutation of Gödel I.
In the primer landmarks this sits at T0 (logic from cost) feeding the T5 uniqueness story ($J(x)=(x+x^{-1})/2-1$) that later pins $\varphi$, the eight-tick octave, and $D=3$. Downstream, the holds theorem and the deprecated alias both route through this structure; t3 empty-ledger bridges sit in parallel at later rungs. Open question touched: module prose still advertises "Gödel dissolved" at the top level, while this declaration’s doc-comment corrects that overclaim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.