Shadow Diagram

The image of a τ-internal commutative diagram under the bridge functor F. The shadow preserves commutativity but may lose structure: each forbidden move introduces a specific degeneracy in the shadow.

Shadow Diagram

Summary

The image of a τ-internal commutative diagram under the bridge functor F. The shadow preserves commutativity but may lose structure: each forbidden move introduces a specific degeneracy in the shadow.

Statement

%
\label{def:shadow-diagram}
Let $\mathcal{D}$ be a commutative diagram
in $\operatorname{Cat}_{\T}(\Elayer{2})$
and $F$ a bridge (Definition~\ref{def:bridge-axiom}).
The \textbf{shadow diagram} $F(\mathcal{D})$
is the image of $\mathcal{D}$ under~$F$.
\begin{enumerate}
\item\emph{(Commutativity.)}
If $g \circ f = h$ in $\mathcal{D}$,
then $F(g) \circ F(f) = F(h)$ in $F(\mathcal{D})$.

\item\emph{(Degeneracy.)}
Each forbidden move $M_{i}$
(Definition~\ref{def:five-forbidden-moves})
introduces a specific degeneracy:
$M_{1}$~collapses objects beyond the $\KAxiom{3}$ bound;
$M_{2}$~identifies objects from different sectors;
$M_{3}$~compresses long $\T$-descriptions into short ZFC-derivations;
$M_{4}$~collapses depth-$k$ distinctions under ZFC quantification;
$M_{5}$~merges objects with different NF addresses
that ZFC re-encodes as identical.
\end{enumerate}

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-03.jsonl line 177
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part10/ch67-the-bridge-axiom.tex lines 142-166

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Bridge.BridgeAxiom
• Name: shadow_diagram_check

Dependencies

• Canonical: III.D71, III.D69

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.