T0_To_CanonicalGodelDissolution_Bridge
plain-language theorem explainer
Deprecated name alias for the T0 bridge that packages classical biconditional self-negation impossibility with the unique cost minimizer at the identity. Anyone citing the old “Gödel dissolution” label should switch to the renamed classical-logic-and-unique-minimizer bridge. The body is a one-line abbrev redirect; no new mathematics is proved here.
Claim. The historical T0 bridge formerly labeled “canonical Gödel dissolution” is definitionally identical to the T0 classical-logic and unique-minimizer bridge: under forced T0 logic, there is no inhabitant of $P \leftrightarrow \neg P$ (in two formulations), stabilization status is definite, and the unique RS cost minimizer is $x = 1$.
background
The Unified Forcing Chain module argues that T0–T8 are forced from the Recognition Composition Law plus normalization and calibration, starting from an absolute floor. T0 is the claim that classical logic emerges from cost minimization (“consistency is cheap”), not an external assumption.
The target of this alias is a Prop-structure conditioned on T0 being forced. Its fields record: no configuration realizing biconditional self-negation $P \leftrightarrow \neg P$; the same fact at general predicate level; definite (decidable) stabilization status; and the substantive unique-minimizer fact tied to T5-style uniqueness at the identity. The module’s older rhetoric said “Gödel dissolved”; the structure docs explicitly retract that reading.
Upstream, the holding theorem builds the bundle from biconditional-self-negation lemmas (no self-negating config, no general self-negating predicate, decidable stabilization) once T0 is given.
proof idea
Pure definitional alias: the abbrev is @ applied to the renamed bridge structure, so the two names are definitionally equal. No tactics, no new fields, no proof obligations. The deprecated attribute points callers to T0_To_ClassicalLogicAndUniqueMinimizer_Bridge. The companion holding theorem (also renamed) is what actually assembles the classical-logic and unique-minimizer conjuncts.
why it matters
Keeps old call sites compiling while the forcing-chain vocabulary drops the false “Gödel dissolution” slogan. The real content sits at T0 in the inevitability ladder: logic-from-cost, plus classical impossibility of $P \leftrightarrow \neg P$, feeding later ledger and recognition steps. Downstream, the T3 canonical empty-ledger bridge holder still touches this naming layer in the chain wiring. Framework-wise this is bookkeeping on the T0 rung, not a new forcing step (T5 J-uniqueness and the unique minimizer $x=1$ are only re-exported, not re-proved here). The open editorial point is already closed in the docs: incompleteness is not refuted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.