\section{Complete Tight-Core Boundary Theorem}\label{sec:boundary-iff}

This section rewrites the reference boundary classification so it is finite and witness-producing.
The theorem stops at the boundary objects that are decidable from finite data: tight-core type, face-map consistency,
and Doeblin-word existence.

Recurrence along a chosen minimizing trajectory is a separate layer and is used only under explicit recurrence inputs.


\begin{definition}[Obstruction gates (OG1--OG4)]\label{def:og}
The finite boundary analysis is organized around four obstruction gates.
\begin{itemize}[leftmargin=2em]
\item \textbf{OG1:} every tight SCC is imprimitive ($\mathrm{per}(H)>1$), so no aperiodic tight core exists.
\item \textbf{OG2:} an aperiodic tight SCC exists, but active-face consistency fails (Definition~\ref{def:face-map}), producing a cycle witness (Lemma~\ref{lem:og2-witness-cycle}).
\item \textbf{OG3:} a consistent active face exists, but there is no Doeblin word on that face; this yields a finite cut or product-automaton non-reachability witness (Algorithm~\ref{alg:doeblinword}).
\item \textbf{OG4:} a Doeblin word exists, but it is not recurrent along the tight dynamics; this yields an explicit avoidance-cycle witness (Lemma~\ref{lem:avoidance-cycle-witness}) and is formalized as Definition~\ref{def:og4}.
\end{itemize}
\end{definition}

\begin{corollary}[Obstruction witnesses are explicit]\label{thm:og-witness}
If any obstruction gate from Definition~\ref{def:og} holds, then the certificate pipeline produces a finite, checkable witness object (cycle, cut, automaton non-reachability, or avoidance cycle).
In particular, in the presence of an obstruction gate, no gap-free Doeblin\,+\,recurrence contraction conclusion can be asserted on the corresponding tight core.
\end{corollary}

\begin{theorem}[Complete Tight-Core Boundary Theorem (finite, witness-producing form)]\label{thm:complete-tight-core-boundary}
Let $G^{(0)}$ be the tight graph associated to a calibrated potential (Definition~\ref{def:tight}).
Then exactly one of the following holds.

\begin{itemize}
\item[(OG1) \textbf{Imprimitive-only tight core.}]
Every SCC $H$ of $G^{(0)}$ is imprimitive, i.e.\ $\mathrm{per}(H)>1$ (Definition~\ref{def:period}).
A finite witness is the SCC decomposition of $G^{(0)}$ together with the computed periods $\mathrm{per}(H)$.

\item[(A) \textbf{An aperiodic tight SCC exists.}]
There exists an aperiodic SCC $H$ of $G^{(0)}$, i.e.\ $\mathrm{per}(H)=1$.
Fix such an $H$.
Then exactly one of the following holds on $H$.

\begin{itemize}
\item[(OG2) \textbf{Active-face instability on $H$.}]
The descriptor reduction fails to provide a consistent face map on $H$ (Definition~\ref{def:face-map}).
A finite witness is a directed cycle word in $H$ with marked indices $(i,j)$ witnessing spurious activation,
as in Lemma~\ref{lem:og2-witness-cycle}.

\item[(OG3) \textbf{No Doeblin word on the active face of $H$.}]
A consistent face map exists on $H$ with active face $S(H)$, but there is no word $w$ supported in $H$
whose face-restricted block product is strictly positive on $S(H)\times S(H)$.
A finite witness is either
\begin{itemize}
\item a cut witness showing $\Gamma(H)$ is not strongly connected, or
\item a Boolean-pattern product-automaton non-reachability certificate for the all-ones pattern state $(v_0,\mathbf{1})$
produced by Algorithm~\ref{alg:doeblinword}.
\end{itemize}

\item[(\textbf{Doeblin}) \textbf{A Doeblin word is certified on $H$.}]
There exists a word $w$ supported in $H$ such that the face-restricted block product $B(w)$ is strictly positive on
$S(H)\times S(H)$.
Equivalently, the Boolean-pattern product-automaton test reaches a return state $(v_0,\mathbf{1})$ and returns an explicit witness word $w$
(Corollary~\ref{cor:doeblin-from-cert}).
The witness object is the triple $(H,S(H),w)$.
\end{itemize}
\end{itemize}

Moreover, if a minimizing path $\pi$ admits an aperiodic tight SCC in its tight-core dichotomy (Proposition~\ref{prop:tight-dichotomy}),
then applying the aperiodic branch above to that SCC returns a finite boundary object: an explicit OG2 witness,
an explicit OG3 witness, or an explicit Doeblin word witness.
\end{theorem}

\begin{proof}[Proof map]
Compute the SCC decomposition of $G^{(0)}$ and the period $\mathrm{per}(H)$ of each SCC (Definition~\ref{def:period}).
If all SCCs satisfy $\mathrm{per}(H)>1$, we are in (OG1).
Otherwise, fix an aperiodic SCC $H$.

Face-map consistency on $H$ is a finite check on the template sparsity patterns and yields an explicit inconsistency cycle witness
when it fails (Lemma~\ref{lem:og2-witness-cycle}).
Assuming a consistent face map, Doeblin-word existence on $S(H)$ is equivalent to reachability of a return state $(v_0,\mathbf{1})$
in the Boolean-pattern product automaton.
Algorithm~\ref{alg:doeblinword} returns either an explicit witness word $w$ or a finite non-reachability certificate
(Corollary~\ref{cor:doeblin-from-cert}).
These outcomes are mutually exclusive and exhaustive, yielding (OG2), (OG3), or (\textbf{Doeblin}).

Finally, Proposition~\ref{prop:tight-dichotomy} identifies when a minimizing path supplies an aperiodic tight SCC to which the aperiodic branch applies.
\end{proof}
