FPRD-T166: Finite-state causal preimages preserve stationary transport

1. Synchronous causal recodings

Let

$$T=(S,s_0,\mu,\lambda)$$

be a deterministic synchronous Mealy transducer from input alphabet $\Sigma$ to output alphabet $\Gamma$. Thus

$$\mu:S\times\Sigma\to S, \qquad \lambda:S\times\Sigma\to\Gamma,$$

and one output letter is produced for each input letter. Write $T(w)\in\Gamma^*$ for the resulting length-preserving causal map.

For a language $L\subseteq\Gamma^*$, its causal preimage is

$$T^{-1}(L)=\{w\in\Sigma^*:T(w)\in L\}.$$

2. The theorem

If

$$(d,k,g,q)\in\operatorname{Tr}(L)$$

and $|S|=s$, then

$$(d,k,g,sq)\in\operatorname{Tr}(T^{-1}(L)).$$

The compiled presentation has exactly the same persistent graph as the source presentation. Only finite control changes.

Proof

Let $A$ be a scaffolding automaton for $L$. The compiled control is a pair $(t,r)$, where $t\in S$ is the current transducer state and $r$ is the current control of $A$.

Suppose the next input symbol is $a$. Compute

$$b=\lambda(t,a), \qquad t'=\mu(t,a).$$

Apply the transition of $A$ for output letter $b$, source control $r$, and the current radius-$k$ scaffold view. Append exactly the label and port descriptors selected by that source transition, and enter compiled control $(t',r')$.

Induction on the input length proves two simultaneous invariants:

1. the compiled scaffold is identical to the scaffold built by $A$ on $T(w)$;
2. the compiled control is the pair of the transducer state after $w$ and the control of $A$ after $T(w)$.

The compiled machine therefore accepts $w$ exactly when $A$ accepts $T(w)$. Degree, descriptor distance, and working alphabet are unchanged, while the control set has at most $sq$ elements.

3. Composition and reversible changes of coordinates

The construction is functorial. If $U$ and $T$ are composable synchronous transducers, then the staged product compiler and the compiler for $T\circ U$ produce the same source scaffold and the same three finite-state components, up to reassociation.

If $T$ is a bijection on words and its inverse is also computed by a finite synchronous transducer, then

$$\operatorname{Tr}(L)\ne\varnothing \quad\Longleftrightarrow\quad \operatorname{Tr}(T^{-1}(L))\ne\varnothing.$$

Thus scaffold recognizability, and equivalently finite stationary transport, is invariant under finite-state synchronous causal changes of coordinates. The individual resource tuples need not be invariant because the forward and inverse transducers add finite control.

4. Why forgotten-action projection is different

For a tagged alphabet $\widehat\Sigma=\Sigma\times S$, forgetting the tag is a letter map

$$\pi:\widehat\Sigma^*\to\Sigma^*.$$

But the forgotten-action language is a direct image:

$$\pi(A)=\{w:\exists\widehat w\in A, \ \pi(\widehat w)=w\}.$$

Membership requires existential choice among hidden tag histories. It is not the inverse image of a deterministic causal recoding of the observed word. FPRD-T166 therefore does not conflict with FPRD-T164. Instead it locates the source of the failure: deterministic finite-state preprocessing is harmless, while existentially merging hidden histories can destroy bounded stationary transport.

5. Verification boundary

The accompanying checker exhausts small Mealy transducers and finite local machines. It compares the source run on $T(w)$ with the product run on $w$, including control, local action trace, evolving abstract view, and acceptance. It separately checks invertible binary Mealy machines against their explicit synchronous inverses.

This checker tests the product identity, not every scaffolding automaton. The proof above is the general argument. Product constructions and inverse-image closure under deterministic finite-state transductions are standard automata ideas. The contribution here is the exact unchanged-graph transport bound and its use in separating causal recoding from forgotten-action projection. No literature-priority or independent-review claim is made.