\label{prop:bridgehead-proposition}
Let $\operatorname{Agent}(\Elayer{2})$ denote the category of $\Elayer{2}$
computational agents.  Then:
\begin{enumerate}
\item[\emph{(i)}] \textbf{Necessity.} Every $\Elayer{2}$ agent restricts to a
proto-code: the forgetful functor
$U : \operatorname{Agent}(\Elayer{2}) \to \operatorname{Proto}(\Elayer{1})$
that discards the decoder is well-defined and faithful.

\item[\emph{(ii)}] \textbf{Non-sufficiency.} The functor $U$ is not
essentially surjective: there exist proto-codes that are not the underlying
carrier of any $\Elayer{2}$ agent.

\item[\emph{(iii)}] \textbf{Non-triviality criterion.}
$\operatorname{Agent}(\Elayer{2})$ is non-empty only if
$\operatorname{Proto}(\Elayer{1})$ contains non-torsion objects.
Equivalently, $\Elayer{2}$ emergence requires $r_\infty > 0$, which by the
BSD functional is equivalent to $\operatorname{BSD}_{\T}(k_*) \neq 0$.
\end{enumerate}