FPRD-T173: Effective selection horizons for regular hidden sources

1. Setting

Let

$$A\subseteq\widehat\Sigma^*$$

be accepted by a complete DFA with $r$ states, and let

$$\pi:\widehat\Sigma\to\Sigma$$

be a letter projection. Fix a family

$$F=(T_1,\ldots,T_m)$$

of projection-compatible synchronous selectors. Each selector is a total Mealy machine with at most $s$ states. The family covers the accepting lifts when

$$\pi(A)=\bigcup_{i=1}^m T_i^{-1}(A).$$

The inclusion from right to left is automatic because $\pi(T_i(w))=w$. The only possible failure is therefore an observed word that has some accepting lift in A but whose selected lifts all fail.

2. The missed-word automaton

For a fixed family F, construct an NFA $P_F$ over $\Sigma$. Its state is

$$\left(p;(t_1,q_1),\ldots,(t_m,q_m)\right).$$

Here:

• p is a state of the source DFA reached by one nondeterministically chosen hidden lift;
• $t_i$ is the current state of selector $T_i$;
• $q_i$ is the source-DFA state reached by the lift emitted by $T_i$.

On observed letter x, the NFA chooses $\widehat x\in\pi^{-1}(x)$ for the source coordinate. Each selector coordinate advances deterministically and feeds its emitted tagged letter to its own copy of the source DFA.

A product state is accepting exactly when p is accepting and every $q_i$ is rejecting. Hence

$$L(P_F) =\pi(A)\setminus\bigcup_{i=1}^mT_i^{-1}(A).$$

After padding smaller selectors with unreachable states, the product has at most

$$N(r,m,s)=r(rs)^m=r^{m+1}s^m$$

states.

3. FPRD-T173: effective finite-horizon collapse

The family F covers $\pi(A)$ globally if and only if it covers every accepted observed word of length at most

$$H(r,m,s)=r^{m+1}s^m-1.$$

Proof

If F is not a global cover, $P_F$ accepts a word. A shortest accepting run cannot repeat a product state, since deleting the intervening cycle would give a shorter accepting run. Because $P_F$ has at most N states, the word has length at most $N-1$. The converse is immediate.

Equivalently, for the resource spectrum of FPRD-T169,

$$(m,s)\in\operatorname{Sel}(A,\pi) \quad\Longleftrightarrow\quad (m,s)\in\operatorname{Sel}_{H(r,m,s)}(A,\pi).$$

The selector family witnessing the finite-horizon statement is already a global witness. This is stronger than merely saying that every failed family has some finite counterexample.

4. Effective obstruction suites

If the budget $(m,s)$ is infeasible, every candidate family has a shortest missed word of length at most H. Choosing one such word for each candidate family and removing duplicates gives a T171 obstruction suite W satisfying

$$\max_{w\in W}|w|\le H(r,m,s), \qquad |W|\le N_{m,s}(\pi).$$

Thus, for a regular hidden source, both certificate resources become effectively bounded:

$$e_{A,\pi}(m,s)\le r^{m+1}s^m-1, \qquad \omega_{A,\pi}(m,s)\le N_{m,s}(\pi).$$

One can decide whether $(m,s)$ is feasible by enumerating the finite selector-family universe and testing the corresponding missed-word automata for emptiness. The theorem is an explicit bounded-budget decision procedure, not an efficient one.

5. Relation to the preceding theory

FPRD-T169 proves finite escape for arbitrary hidden source languages by compactness of the finite selector universe. It supplies no uniform escape length. FPRD-T171 bounds obstruction cardinality but not obstruction radius. FPRD-T172 identifies regular source presentations with domain-covering multi-sequential uniformization.

T173 is the effective regular-source specialization of those three results. Regularity makes the failure language for each candidate family finite-state, so the infinite coverage question collapses to one explicit horizon.

This is also a useful boundary for the hard visible lift in FPRD-T168. That lift is deterministic visibly pushdown rather than regular. T173 therefore does not supply a uniform bound for its escape function. Any such bound must use pushdown structure beyond ordinary finite-state products.

6. Evidence and limits

The checker exhausts all 1,024 complete two-state DFAs over the binary tagged alphabet. It checks every family of one or two one-state selectors, and every single two-state selector. For each case it builds the missed-word product, verifies the state bound, and confirms that every nonempty failure language has a shortest witness below the theorem horizon.

Limits:

• The bound counts labeled product states and need not be tight.
• The result fixes both selector count and selector state size.
• It covers synchronous letter projections, not asynchronous transducers.
• It does not produce a computable escape bound for nonregular source presentations such as the hard visibly pushdown lift.
• The proof is an elementary finite-automaton product and shortest-path argument. No literature-priority claim is made without specialist review.