% doeblin_word_search.tex
% Finite-state discovery of a Doeblin word on an active face via a Boolean-pattern product automaton.

\section{Doeblin-word discovery by a finite product automaton}
\label{sec:doeblin-word-search}

This section records the finite-state procedure used throughout the certificate pipeline to decide whether a given aperiodic tight SCC admits a Doeblin word on its active face.
The input is purely combinatorial support information on the face, and the output is either a concrete witness word or a finite non-reachability certificate.

\subsection{Boolean patterns and Boolean product}
\label{subsec:boolean-patterns}

Fix a tight SCC $H$ and a face $S=S(H)\subseteq\{1,\dots,d\}$.
For each tight edge $e:u\to v$ in $H$, let $B_e\in\mathbb{R}^{d\times d}_+$ denote the corresponding nonnegative block (or fixed-length template).
Define the face-restricted support pattern
\[
P_e\in\{0,1\}^{S\times S},\qquad (P_e)_{ij}=1\ \Longleftrightarrow\ (B_e)_{ij}>0\ \text{for } i,j\in S.
\]
For Boolean patterns $P,Q\in\{0,1\}^{S\times S}$, define their Boolean product $P\odot Q$ by
\[
(P\odot Q)_{ij}=\bigvee_{k\in S}\bigl(P_{ik}\wedge Q_{kj}\bigr),
\]
so that $P\odot Q$ records the support pattern of the matrix product of the underlying nonnegative blocks restricted to $S$.

\subsection{The product automaton and BFS search}
\label{subsec:product-automaton}

Let $\mathcal{P}:=\{0,1\}^{S\times S}$ be the finite set of Boolean patterns.
The product automaton has state space $H\times\mathcal{P}$.
A directed transition
\[
(u,P)\ \xrightarrow{\ e:u\to v\ }\ (v,P_e\odot P)
\]
records the effect of appending the edge $e$ to the front of the word whose current pattern is $P$.

\begin{algorithm}[H]
\caption{Doeblin-word discovery by finite product automaton}\label{alg:doeblinword}
\begin{algorithmic}[1]
\Require Tight SCC $H$, active face $S(H)$, Boolean support patterns $P_e$ on $S(H)$ for each tight edge $e$ in $H$
\Ensure Either a word $w$ whose face-restricted product is strictly positive, or a finite non-reachability certificate
\State Choose a base vertex $v_0\in H$
\State Let $I$ be the identity pattern on $S(H)$ and let $\mathbf{1}$ denote the all-ones pattern on $S(H)\times S(H)$
\State Initialize BFS on states $(v,P)$ with the start state $(v_0,I)$
\While{queue not empty}
  \State Pop $(u,P)$
  \ForAll{tight edges $e:u\to v$ in $H$}
    \State $P'\gets P_e\odot P$
    \If{$(v,P')$ not yet visited}
      \State Mark visited; record predecessor; enqueue $(v,P')$
    \EndIf
    \If{$v=v_0$ \textbf{and} $P'=\mathbf{1}$}
      \State Reconstruct the witnessed word $w$ from predecessors and \Return $w$
    \EndIf
  \EndFor
\EndWhile
\State \Return finite non-reachability certificate: $\mathbf{1}$ is not reachable at $(v_0,\cdot)$
\end{algorithmic}
\end{algorithm}

\begin{remark}[Complexity]
The state space has size $|H|\cdot 2^{|S(H)|^2}$.
This exponential dependence on the face size is unavoidable at the level of brute-force semigroup reachability, but in the intended regime the active faces are descriptor-controlled and small.
\end{remark}

\begin{remark}[Language-aware reachability versus conservative support filters]
In some implementations it is convenient to precompute auxiliary reachability graphs from template support information that are (intentionally) conservative.
Such over-approximations may make the presentation look looser than necessary, but they do not affect correctness:
the decisive Doeblin step is the product-automaton decision above, which is built from the actual tight-language edges in $H$ and the face-restricted patterns $P_e$.
Any word returned by Algorithm~\ref{alg:doeblinword} is a valid witness on the declared face, and any non-reachability conclusion is only asserted for the declared automaton.
\end{remark}
