Bounded-role causal certificates at one supplied cut

Status: proof draft. This is the causal-realizability companion to the target-owned cone-partition theorem. It concerns a fixed future horizon and a configuration supplied at the cut; it is not an online sewing theorem and makes no novelty claim.

1. Fixed read doctrine

Let $\Sigma$ and $Y$ be nonempty finite sets and let $f:\Sigma^*\to Y$. Fix a horizon $H\ge0$ and a track count $k\ge0$.

For a frozen old prefix $u$, a track address lies in

$$\overline{\mathbb Z}_u=\{\bot\}\cup\{0,\ldots,|u|-1\},$$

where $\bot$ is inactive. An active track may hold or recede by one address, stopping at $0$; an inactive track remains inactive. Tracks cannot be born, move right, or enter the subsequently arriving suffix.

The target-independent finite read primitive is

$$\operatorname{rd}_u(p)= \begin{cases} u[p],&p\ne\bot,\\ \dagger,&p=\bot, \end{cases}$$

and

$$\operatorname{obs}_u(\mathbf p) = \bigl(\operatorname{rd}_u(p_1),\ldots, \operatorname{rd}_u(p_k)\bigr) \in D^k, \qquad D=\Sigma\cup\{\dagger\}. \tag{1}$$

This draft pins exactly the observation alphabet $D^k$ in (1). A different finite sensor package defines a different doctrine and changes the factor $|D|^k$ in the counting bound. The controller does not receive raw integer addresses or the old prefix as an atomic value.

2. Cut-initialized controller

A deterministic $k$-track continuation controller has a finite state set $Q$ and maps

$$\delta:Q\times\Sigma\times D^k \longrightarrow Q\times\{\mathsf H,\mathsf R\}^k, \qquad \omega:Q\times D^k\longrightarrow Y. \tag{2}$$

Here $\mathsf H$ means hold and $\mathsf R$ means recede, with receding at address $0$ interpreted as holding.

For every old prefix $u$, the controller is supplied with a cut initialization

$$(q_u,\mathbf p_u)\in Q\times\overline{\mathbb Z}_u^k.$$

At a continuation node $v$, it outputs

$$\omega(q_{u,v},\operatorname{obs}_u(\mathbf p_{u,v})).$$

On the next symbol $a$, it applies (2), then moves the tracks as directed. It is correct through $H$ when this output equals $f(uv)$ for every $|v|\le H$.

Nothing here explains how $(q_u,\mathbf p_u)$ was reached. It is supplied cut data.

3. Forward factorization

Define the bounded residual row

$$r_H(u)(v)=f(uv), \qquad v\in\Sigma^{\le H},$$

and let

$$Q_H(f)=\{r_H(u):u\in\Sigma^*\}.$$

For $q\in Q$, define its depth-$h$ causal role recursively. At depth zero,

$$s_0(q)=\bigl(z\mapsto\omega(q,z)\bigr). \tag{3}$$

For $h\ge1$, if

$$\delta(q,a,z)=(q',\mu(q,a,z)),$$

put

$$s_h(q)= \left( s_0(q), \bigl(\mu(q,a,z),s_{h-1}(q')\bigr)_ {a\in\Sigma,\ z\in D^k} \right). \tag{4}$$

Let $C_h=s_h(Q)$, tagging different grades if necessary. Then $|C_h|\le|Q|$.

For the run after $u$, define its causal observation channel

$$\chi_u(v) = \operatorname{obs}_u(\mathbf p_{u,v}), \qquad v\in\Sigma^{\le H}. \tag{5}$$

Theorem 1 — controller factorization

There is a uniform interpreter $\Phi_H$ such that

$$\boxed{ r_H(u)=\Phi_H(s_H(q_u),\chi_u) } \tag{6}$$

for every $u$. Consequently the code image maps surjectively onto the bounded residual quotient:

$$\{(s_H(q_u),\chi_u):u\in\Sigma^*\} \twoheadrightarrow Q_H(f). \tag{7}$$

In particular, with

$$N_H=|\Sigma^{\le H}|,$$

$$|Q_H(f)| \le |C_H|\,|D|^{kN_H}. \tag{8}$$

Proof

Starting from $s_H(q_u)$, equation (4) says how the finite role changes for every next symbol once the current observation from (5) is supplied. It also gives the move vector. Repeating this through the continuation tree recovers the role at every node. Equation (3), together with that node’s observation, then recovers the output. These outputs are exactly $r_H(u)$ by correctness. Equation (7) follows because every bounded residual has a prefix witness. There are at most $|D|^{kN_H}$ possible channel trees, which gives (8). $\square$

The channel in (5) is the complete counterfactual continuation-tree transcript: it records what the tracks would read on every suffix through $H$, not only on one realized suffix. It is presentation-dependent, but it is not an arbitrary label: it has a witness consisting of $k$ legal old-address trajectories and literal reads under (1). The supplied cut initialization may still be arbitrary target-dependent advice; this theorem does not make it online.

4. Converse certificate

A depth-$H$ causal certificate supplies, for every old prefix $u$ and every $v\in\Sigma^{\le H}$,

$$c_u(v)\in C_{H-|v|}, \qquad \mathbf p_u(v)\in\overline{\mathbb Z}_u^k, \qquad z_u(v)=\operatorname{obs}_u(\mathbf p_u(v)), \tag{9}$$

where each $C_h$ is finite. For every edge $v\to va$ with $|v|<H$, it also supplies a move vector $\mu_u(v,a)$.

Require:

1. Track provenance. Applying $\mu_u(v,a)$ to $\mathbf p_u(v)$ gives $\mathbf p_u(va)$, using only legal hold/recede moves.
2. Uniform readout. At nodes of the same remaining grade, $$(c_u(v),z_u(v))=(c_{u'}(v'),z_{u'}(v')) \Longrightarrow f(uv)=f(u'v'). \tag{10}$$
3. Local transition consistency. At nodes of the same positive remaining grade $h\ge1$, equality of the pair $(c,z)$ implies, for every next symbol $a$, equality of both the move vector and the next role: $$\mu_u(v,a)=\mu_{u'}(v',a), \qquad c_u(va)=c_{u'}(v'a). \tag{11}$$

Theorem 2 — certificate compilation

Every certificate satisfying (9)–(11) compiles into a finite $H$-specific controller that is strict layered through the promised horizon. From the supplied root initialization $(c_u(\varepsilon),\mathbf p_u(\varepsilon))$, it realizes $f(uv)$ for every $|v|\le H$. Its layer-width coordinate is

$$\max_{0\le h\le H}|C_h|, \tag{12}$$

while its actual total number of grade-tagged states is

$$\sum_{h=0}^H|C_h|, \tag{13}$$

plus one post-horizon sink if a total transition function beyond $H$ is required.

Proof

Tag the sets $C_h$ by their remaining grade and take their disjoint union as the controller state set. The root state is therefore explicitly $H$-tagged: this is a horizon-specific countdown controller. Equation (10) makes one output table on the attained pairs $(c,z)$ well-defined. Equation (11) makes one transition and move table on the attained triples $(c,z,a)$ well-defined. Fill unattained entries within grades $h\ge1$ arbitrarily while preserving the grade decrease. Transitions after a grade-zero leaf are outside the promised horizon; send them to one sink if a total transition function is required.

Induction on $|v|$ shows that the compiled controller has state $c_u(v)$, addresses $\mathbf p_u(v)$, and observation $z_u(v)$ at every node. Equation (10) then gives the correct output. $\square$

Corollary 2a — the reverse construction

Every correct controller of Section 2 yields a certificate by taking

$$c_u(v)=s_{H-|v|}(q_{u,v}),$$

and using its actual addresses, reads, and move vectors. Equations (3)–(4) give uniform readout and local transition consistency. Therefore existence of a controller is equivalent to existence of a certificate at the level of fixed-horizon cut realizability.

The resource statement is asymmetric but exact: the forward construction has $|C_h|\le|Q|$ at every grade, while compilation preserves maximum layer width and may use the state sum (13). It does not preserve the total unlayered state count.

5. The four degeneracies

The theorem becomes empty if any of the following is left unbounded or unconstrained.

5.1 No role budget

Every target has a zero-track certificate:

$$C_h=Q_h(f), \qquad \omega_h(r)=r(\varepsilon), \qquad \delta_{h,a}(r)(v)=r(av). \tag{14}$$

Existence at one finite horizon therefore carries no information. A substantive section fixes $k$ and a bound on $|C_h|$, preferably uniformly in $H$.

5.2 Arbitrary channel labels

If $\chi_u$ need not be generated by literal reads at legal addresses, it can carry the entire residual table.

5.3 Target-dependent or unbounded sensors

If one read may return $u$, $r_H(u)$, or an unrestricted raw integer, one track can encode the answer. The fixed, finite, target-independent read primitive is load-bearing.

5.4 Pathwise legality without local consistency

Each prefix may have a separately legal trajectory tree while using hidden prefix information to choose different moves at identical local tuples. Such data do not compile to one controller. Equation (11) is the causal realizability condition.

6. The unsolved sewing seam

The two theorems concern a supplied cut initialization and one finite horizon. They do not show:

• that the root code and positions can be produced causally from the old prefix;
• that certificates at neighboring cuts are compatible;
• that controllers chosen separately for every $H$ come from one horizon-independent presentation.

The quantifier distinction is

$$\forall H\;\exists P_H \quad\not\Longrightarrow\quad \exists P\;\forall H.$$

A full FPRD sewing theorem must add named cut witnesses, one-symbol bonds, diagonal compatibility, and either a finite uniform plateau or a justified compact-stratum argument.

7. Relation to the target-owned cone field

The cone-resolution field and Theorem 1 of cone-factorization-state-track-frontier.md compute an intrinsic fixed-cut snapshot/track frontier. The channel factorization here answers a different question: when does detailed finite-horizon observation data compile to a locally governed controller?

The two theorems do not yet form one proved implication. Their domains also differ: the cone theorem uses a selected equal-length prefix family and one exact continuation length, whereas this note ranges over all old-prefix lengths and all continuations through $H$. The intended optimization bridge must first be stated on a common fixed $(m,H)$ domain and its resource blow-up proved.

The resulting research program has three levels:

$$\boxed{ \begin{array}{c} \text{target-owned resolving field}\\ \dashrightarrow\\ \text{locally consistent bounded-role certificate}\\ \dashrightarrow\\ \text{horizon-independent online presentation} \end{array}}$$

The first dashed arrow is the still-unproved doctrine-specific optimization bridge. The second is the open sewing problem.