\label{prop:sector-instantiation-lemma}
Let $S \in \{A, B, C, D\}$ be a primitive sector and $k \in \{1, 2, 3\}$ an enrichment level.  The sector restriction $\operatorname{Enr}^k|_{S}$ satisfies:
\begin{enumerate}
\item\emph{(Closure.)} $\operatorname{Cat}_{\T}(\Elayer{k})|_{S}$ is a full subcategory of $\operatorname{Cat}_{\T}(\Elayer{k})$, closed under the categorical operations inherited from $\operatorname{Cat}_{\T}(\Elayer{k})$.

\item\emph{(Faithfulness.)} The restriction $\operatorname{Enr}^k|_{S}$ is faithful: distinct $\Elayer{0}$-objects with sector address~$S$ map to distinct $\Elayer{k}$-objects.

\item\emph{(Coherence.)} The diagram
\[
\begin{array}{ccc}
\operatorname{Cat}_{\T}(\Elayer{0})\big|_{S}
  & \xrightarrow{\;\operatorname{Enr}^k|_{S}\;}
  & \operatorname{Cat}_{\T}(\Elayer{k})\big|_{S} \\[6pt]
\big\downarrow\vcenter{\rlap{\scriptsize incl}} & & \big\downarrow\vcenter{\rlap{\scriptsize incl}} \\[6pt]
\operatorname{Cat}_{\T}(\Elayer{0})
  & \xrightarrow{\;\operatorname{Enr}^k\;}
  & \operatorname{Cat}_{\T}(\Elayer{k})
\end{array}
\]
commutes: enriching then restricting equals restricting then enriching.

\item\emph{(Sub-theory completeness.)} Every morphism in $\operatorname{Cat}_{\T}(\Elayer{k})|_{S}$ is the image under $\operatorname{Enr}^k|_{S}$ of a morphism in $\operatorname{Cat}_{\T}(\Elayer{0})|_{S}$, composed with intra-sector structure earned at level~$\Elayer{k}$.
\end{enumerate}