
% descriptor_face_certificates.tex
\section{Descriptor Faces as Finite Certificates (Eliminating Interface Assumptions)}

Two interface notions recur throughout the gap-free theory on a tight SCC $H$: \emph{active-face invariance} and \emph{support-connectivity on the active face}.
In this section we turn both into purely \emph{finite, checkable certificates} extracted directly from the reduced descriptor graph and template sparsity.

\subsection{Canonical active face per descriptor state}

In the descriptor reduction, each vertex $v\in V$ corresponds to a finite descriptor encoding which coordinates
are \emph{potentially active} and which are structurally zero under admissible propagation.
Accordingly, each descriptor vertex carries a canonical support set
\[
S(v)\subseteq \{1,\dots,d\}.
\]

\begin{definition}[Face map and canonical active set]\label{def:face-map}
A \emph{face map} for the reduced graph is a function $S:V\to 2^{\{1,\dots,d\}}$ such that for each edge $e:u\to v$
labeled by a template (or fixed-length block) $T_e$ we have:
\begin{itemize}
\item[(i)] (\textbf{Forward invariance}) $T_e(\mathbb{R}^{S(u)}_{>0})\subseteq \mathbb{R}^{S(v)}_{>0}$;
\item[(ii)] (\textbf{No spurious activation}) If $x\in \mathbb{R}^{S(u)}_{>0}$, then $(T_e x)_i =0$ for all $i\notin S(v)$.
\end{itemize}
\end{definition}

\begin{remark}
Definition \ref{def:face-map} is checkable from template sparsity: it amounts to verifying that the support pattern of each $T_e$
maps the indicator of $S(u)$ into $S(v)$.
\end{remark}

\subsection{Face stability on SCCs as a finite fixed-point}

\begin{lemma}[SCC face stability by intersection closure]\label{lem:scc-face-stability}
Let $H$ be an SCC of the reduced graph and let $S:V\to 2^{\{1,\dots,d\}}$ be a face map.
Define the SCC face by
\[
S(H):=\bigcap_{v\in H} S(v).
\]
Then for every edge $e:u\to v$ inside $H$,
\[
T_e(\mathbb{R}^{S(H)}_{>0})\subseteq \mathbb{R}^{S(H)}_{>0}.
\]
\end{lemma}

\begin{proof}
Since $S(H)\subseteq S(u)$ for each $u\in H$, we have $\mathbb{R}^{S(H)}_{>0}\subseteq \mathbb{R}^{S(u)}_{>0}$.
By forward invariance, $T_e(\mathbb{R}^{S(u)}_{>0})\subseteq \mathbb{R}^{S(v)}_{>0}$.
Because $S(H)\subseteq S(v)$, restricting to coordinates in $S(H)$ yields invariance on $S(H)$.
\end{proof}

\subsection{Support-connectivity on the SCC face as a finite graph property}

Fix an SCC $H$ and its canonical face $S(H)$.
For each generator edge $e$ in $H$ labeled by $T_e$, define the coordinate support digraph on $S(H)$:
we draw an arrow $j\to i$ if there exists an edge $e$ in $H$ with $(T_e)_{ij}>0$.
Thus $j\to i$ records that coordinate $j$ can contribute to coordinate $i$ in one admissible step inside $H$.

\begin{definition}[Coordinate support digraph on a face]\label{def:coord-digraph}
Let $\Gamma(H)$ be the directed graph with vertex set $S(H)$ and an arrow $j\to i$ if there exists an edge $e$ in $H$ such that $(T_e)_{ij}>0$.
\end{definition}

\begin{lemma}[Support-connectivity certificate]\label{lem:support-connectivity}
If $\Gamma(H)$ is strongly connected, then for every $i,j\in S(H)$ there exists an admissible word $w$ in $H$ such that the block product satisfies
$(B(w))_{ij}>0$.
\end{lemma}

\begin{proof}
Strong connectivity gives a coordinate path $j\to \cdots \to i$ realized by a sequence of generator matrices from edges of $H$.
Concatenate the corresponding edges to obtain a word $w$ whose product contains a positive contribution from $j$ into $i$.
\end{proof}

\begin{corollary}[Doeblin word from aperiodic SCC via Boolean-pattern product automaton]\label{cor:doeblin-from-cert}
Let $H$ be an aperiodic SCC of the tight graph $G^{(0)}$ and assume a consistent face map $S(\cdot)$ is available, with active face $S(H)\neq\varnothing$.
Then the following are equivalent:
\begin{itemize}
\item[(i)] There exists a finite word $w$ supported in $H$ such that the block product $B(w)$ is strictly positive on $S(H)\times S(H)$ (equivalently, $w$ is Doeblin on the face $S(H)$).
\item[(ii)] The Boolean-pattern product-automaton test (Algorithm~\ref{alg:doeblinword}) reaches a return state $(v_0,\mathbf{1})$ for some base vertex $v_0\in H$, where $\mathbf{1}$ denotes the all-ones pattern on $S(H)\times S(H)$; in this case the algorithm returns an explicit witness word $w$.
\end{itemize}
In case (i), strict positivity of $B(w)_{S(H)\times S(H)}$ implies that for every $i,j\in S(H)$ there exists a directed coordinate path $j\to\cdots\to i$ in $\Gamma(H)$, hence $\Gamma(H)$ is strongly connected.
Thus failure of strong connectivity produces the OG3 cut witness of Lemma~\ref{lem:og3-witness-cut}, and strong connectivity of $\Gamma(H)$ is a fast necessary check.
When $\Gamma(H)$ is strongly connected, the existence of a Doeblin word is decided by the Boolean-pattern product-automaton test (Algorithm~\ref{alg:doeblinword}); the graph condition alone does not certify strict positivity on $S(H)\times S(H)$.
\end{corollary}


\begin{remark}[Strong connectivity is necessary but not sufficient]\label{rem:gamma-not-sufficient}
Strong connectivity of $\Gamma(H)$ is a fast necessary test for the existence of a Doeblin word.
However, $\Gamma(H)$ records only one-step support reachability and does not encode higher-order pattern constraints that can prevent simultaneous positivity of all pairs.
A clean counter-shape is the permutation case: if all allowed face-restricted patterns are permutation matrices generating a transitive action on $S(H)$,
then $\Gamma(H)$ is strongly connected while every admissible product remains a permutation pattern, so no word yields strict positivity on $S(H)\times S(H)$.
For this reason, the pipeline uses the Boolean-pattern product-automaton test (Algorithm~\ref{alg:doeblinword}) as the definitive finite decision procedure;
when it fails, it returns an explicit finite non-reachability certificate in that automaton.
\end{remark}


\subsection{Algorithmic extraction}

\subsection{Witness extraction when certificates fail}

The obstruction predicates OG2/OG3 are designed to be not merely \emph{named} failures but \emph{witness-producing} ones.
Here we record explicit finite witnesses that can be returned whenever the face-map or coordinate-connectivity
checks fail.

\begin{definition}[Support propagation operator]
For an edge $e:u\to v$ labeled by a nonnegative template/block $T_e$ and a set $S\subseteq\{1,\dots,d\}$,
define the propagated support
\[
\operatorname{Prop}_e(S):=\{\, i:\ \exists j\in S\ \text{with}\ (T_e)_{ij}>0\,\}.
\]
For a word $w=e_1\cdots e_L$ we set $\operatorname{Prop}_w:=\operatorname{Prop}_{e_L}\circ\cdots\circ\operatorname{Prop}_{e_1}$.
\end{definition}

\begin{lemma}[OG2 witness: finite inconsistency cycle]\label{lem:og2-witness-cycle}
Let $H$ be an SCC and suppose the proposed face sets $S(v)$ fail to form a face map on $H$.
Then there exist vertices $u,v\in H$, an edge $e:u\to v$ in $H$, and indices $j\in S(u)$ and $i\notin S(v)$ such that
$(T_e)_{ij}>0$.
Moreover, choosing any directed path $p$ in $H$ from $v$ back to $u$ and setting $w:=ep$, we obtain a directed cycle word $w$
in $H$ together with a marked step (the first step $e$) at which a coordinate outside the designated face is activated.
This pair $(w,(i,j))$ is a finite witness of OG2 on $H$.
\end{lemma}

\begin{proof}
If $S(\cdot)$ is not a face map on $H$, then some edge $e:u\to v$ in $H$ violates Definition~\ref{def:face-map}.
In particular, the ``no spurious activation'' condition (ii) fails, which means exactly that
$\operatorname{Prop}_e(S(u))\nsubseteq S(v)$.
Equivalently, there exist $j\in S(u)$ and $i\notin S(v)$ with $(T_e)_{ij}>0$.
Because $H$ is strongly connected, there exists a directed path $p$ from $v$ to $u$, so $w:=ep$ is a directed cycle word in $H$.
The marked first step $e$ certifies the activation of an outside coordinate along a cycle in $H$.
\end{proof}

\begin{lemma}[OG3 witness: cut decomposition of $\Gamma(H)$]\label{lem:og3-witness-cut}
Let $H$ be a tight SCC for which a face map exists and let $S(H)$ be the SCC face.
If the coordinate digraph $\Gamma(H)$ is not strongly connected, then there exist nonempty disjoint sets
$A,B\subseteq S(H)$ with $A\cup B=S(H)$ such that
\[
(T_e)_{ij}=0\qquad\text{for every edge $e$ in $H$, every $i\in A$, and every $j\in B$.}
\]
Equivalently, $\Gamma(H)$ has no directed edges from $B$ to $A$.
In particular, for every admissible word $w$ in $H$ and every $i\in A$, $j\in B$ we have $(B(w))_{ij}=0$.
Thus $(H,S(H),A,B)$ is a finite witness of OG3.
\end{lemma}

\begin{proof}
Compute the SCC decomposition of $\Gamma(H)$ and consider its condensation DAG.
Since $\Gamma(H)$ is not strongly connected, this DAG has at least two nodes and hence has a sink SCC $A$.
Let $B:=S(H)\setminus A$.
By the definition of a sink SCC, there is no directed edge in $\Gamma(H)$ from any vertex in $B$ to any vertex in $A$.
By Definition~\ref{def:coord-digraph}, an edge $j\to i$ in $\Gamma(H)$ exists exactly when some generator edge $e$ in $H$
has $(T_e)_{ij}>0$.
Therefore for all $i\in A$ and $j\in B$, and for all edges $e$ in $H$, we have $(T_e)_{ij}=0$.
The final structural-zero claim for products follows by closure under multiplication of nonnegative matrices: if every generator has
zeros on $A\times B$, then every product does as well.
\end{proof}

\begin{algorithm}[H]
\caption{Compute SCC face and coordinate support graph}
\begin{algorithmic}[1]
\Require SCC $H$ with face map $S(\cdot)$ and generator labels $T_e$
\Ensure $S(H)$ and coordinate digraph $\Gamma(H)$
\State $S(H)\gets \bigcap_{v\in H} S(v)$
\State Initialize $\Gamma(H)$ with vertex set $S(H)$
\ForAll{edges $e$ inside $H$}
\ForAll{$i,j\in S(H)$}
\If{$(T_e)_{ij}>0$} add arrow $j\to i$ \EndIf
\EndFor
\EndFor
\end{algorithmic}
\end{algorithm}

\begin{algorithm}[H]
\caption{Check OG2--OG3 and produce Doeblin/recurrence witnesses}\label{alg:certificate-pipeline}
\begin{algorithmic}[1]
\Require Tight graph $G^{(0)}$, SCC decomposition, period and coordinate digraphs $\Gamma(H)$
\Ensure Either a finite obstruction witness (OG1/OG2/OG3), or a Doeblin witness $w$ together with either a syndetic modulus $L_{\mathrm{syn}}$ (RC1) or an explicit avoidance-cycle witness
\State Compute SCCs of $G^{(0)}$ and their periods $\mathrm{per}(H)$
\For{each aperiodic SCC $H$}
  \State Attempt to compute a consistent face map $S(\cdot)$ on $H$
  \If{inconsistent}
     \State \Return OG2 witness (inconsistency cycle)
  \EndIf
  \State Build $\Gamma(H)$ on $S(H)$
  \If{$\Gamma(H)$ is not strongly connected}
     \State \Return OG3 witness of type (cut) via Lemma~\ref{lem:og3-witness-cut}
  \EndIf
  \State Run the product-automaton Doeblin-word test (Algorithm~\ref{alg:doeblinword})
  \If{Algorithm~\ref{alg:doeblinword} returns a word $w$}
     \State Build the avoidance graph $\mathcal{A}_{\neg w}(H)$ (Definition~\ref{def:avoidance-graph})
     \If{$\mathcal{A}_{\neg w}(H)$ contains a directed cycle}
        \State \Return Doeblin witness $w$ and an avoidance-cycle witness (Lemma~\ref{lem:avoidance-cycle-witness})
     \Else
        \State Compute $L_{\mathrm{syn}}=1+\ell_{\max}$ where $\ell_{\max}$ is the longest path length in $\mathcal{A}_{\neg w}(H)$
        \State \Return $(w,L_{\mathrm{syn}})$ (RC1; Lemma~\ref{lem:avoidance-syndetic})
     \EndIf
  \Else
     \State \Return OG3 witness of type (product-automaton): a finite non-reachability certificate in the Boolean-pattern product automaton (no return state $(v_0,\mathbf{1})$ is reachable)
  \EndIf
\EndFor
\State \Return OG1 witness (no aperiodic SCC exists in $G^{(0)}$)
\end{algorithmic}
\end{algorithm}

