Move-Bridge Correspondence

The bridge functor is faithful on the complement of the five forbidden moves and degenerates precisely at them. Each move corresponds to a specific structural feature the bridge cannot preserve.

Move-Bridge Correspondence

Summary

The bridge functor is faithful on the complement of the five forbidden moves and degenerates precisely at them. Each move corresponds to a specific structural feature the bridge cannot preserve.

Statement

\label{thm:move-bridge-correspondence}
Let $F\colon \operatorname{Cat}_{\T}(\Elayer{2})
\to \operatorname{Mod}(\mathrm{ZFC})$ be the bridge functor
(Definition~\ref{def:zfc-as-e2-vm}, Ch.~64), and let
$\{M_{1}, \ldots, M_{5}\}$ be the five forbidden moves
(Definition~\ref{def:five-forbidden-moves}).
\begin{enumerate}
\item\emph{(Faithfulness.)}
$F$ restricted to $\operatorname{Cat}_{\T}(\Elayer{2})
 \setminus \bigcup_{i} \operatorname{ker}(M_{i})$ is faithful.

\item\emph{(Degeneration.)}
For each $i$, there exist $X_{i} \neq Y_{i}$ with
$F(X_{i}) \cong F(Y_{i})$ in $\operatorname{Mod}(\mathrm{ZFC})$.

\item\emph{(Completeness.)}
Every identification $F(X) \cong F(Y)$ with $X \neq Y$ factors
through $\operatorname{ker}(M_{i})$ for some~$i$.
\end{enumerate}

Proof / Justification

No immediate manuscript proof block was extracted in this pilot run.

Source Context

• Registry source: book-03.jsonl line 173
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part10/ch65-the-five-forbidden-moves.tex lines 187-208

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Bridge.ForbiddenMoves
• Name: move_bridge_check

Dependencies

• Canonical: III.D69, III.D67, III.T41

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.