%
\label{def:bridge-axiom}
A \textbf{bridge} from Category~$\T$ to ZFC is a functor
\begin{equation}\label{eq:ch67-bridge-functor}
F \colon \operatorname{Cat}_{\T}(\Elayer{2})
\;\longrightarrow\; \mathbf{Mod}(\mathrm{ZFC})
\end{equation}
satisfying four properties.
\begin{enumerate}
\item\emph{(i) Carrier preservation.}
For every $\T$-object $X$ with NF address
$a_{X} \in \hat{\mathbb{Z}}_{\T}$,
$F(X)$ is a ZFC-definable set.
If $X \neq Y$ and neither lies
in the kernel of any forbidden move $M_{i}$
(Definition~\ref{def:five-forbidden-moves}),
then $F(X) \ncong F(Y)$.

\item\emph{(ii) Predicate preservation.}
If $\varphi$ is $\T$-derivable, then $F(\varphi)$ is ZFC-derivable:
$\T \vdash \varphi \;\Longrightarrow\;
\mathrm{ZFC} \vdash F(\varphi)$.
The converse does not hold: ZFC may derive statements
whose $\T$-preimages involve forbidden moves.

\item\emph{(iii) Decoder compatibility.}
The bridge interleaves the two address systems:
\[
\begin{tikzcd}[column sep=large]
\operatorname{Cat}_{\T}(\Elayer{2})
    \ar[r, "F"]
    \ar[d, "\mathrm{NF}"']
& \mathbf{Mod}(\mathrm{ZFC})
    \ar[d, "{\ulcorner\cdot\urcorner}"] \\
\hat{\mathbb{Z}}_{\T}
    \ar[r, "\phi"']
& \mathbb{N}
\end{tikzcd}
\]
commutes up to the decoder map
$\phi \colon \hat{\mathbb{Z}}_{\T} \to \mathbb{N}$,
which sends NF addresses
to G\"odel numbers of the corresponding ZFC-translations.

\item\emph{(iv) Invariant reflection.}
The bridge maps the $\T$-invariant (primorial coherence)
to a sub-statement of the ZFC-invariant (consistency):
$F(\mathrm{Coh}_{\T}) \vdash
\mathrm{Con}(\mathrm{ZFC} \!\upharpoonright\! \operatorname{Im}(F))$.
\end{enumerate}
The bridge is \emph{lossy}:
$\T$-structures with no ZFC counterpart
(primorial tower, earned enrichment, ABCD decomposition)
are projected away;
ZFC-structures with no $\T$-counterpart
(unbounded powerset, global choice)
are absent from $\operatorname{Im}(F)$.