Finite-horizon response capacity of scaffolding automata

Status: self-contained FPRD theorem for the Loff–Moreira–Reis scaffolding-automaton model, with an exact finite audit. No literature-priority claim is made. The theorem combines the published local-neighbourhood semantics with FPRD-T152 cut-response factorization.

1. Model and question

Fix a scaffolding automaton

$$\mathcal A=\langle\Sigma,d,\Gamma,k,Q,\delta,q_0,F\rangle.$$

Its transition at each input symbol sees the finite control state and the radius-$k$ unfolded neighbourhood of the current top. It appends one labelled node. Each of the new node’s $d$ ports is missing, is a self-loop, or points to the endpoint of a port word of length at most $k$ evaluated from the old top.

Fix a cut after some prefix. We ask how much of the old scaffold can affect acceptance under continuations of length at most $h$.

2. Pulling a new neighbourhood backward

Let $N_r(S,v)$ be the radius-$r$ unfolded neighbourhood of node $v$. Physical equality between two endpoints is not part of this observation.

One-step pullback lemma. For $k,r\ge1$, the radius-$r$ neighbourhood of the freshly appended top is determined by:

1. the transition output, and
2. the radius-$(k+r-1)$ neighbourhood of the old top.

Proof. The fresh label is part of the transition output. A path of positive length from the fresh top first uses one fresh port. A missing or self descriptor is already determined. Otherwise that port lands at the endpoint of an old-top word of length at most $k$. At most $r-1$ further old edges are then unfolded. Every required old endpoint therefore lies within radius $k+r-1$ of the old top. Unfolding does not compare endpoint identity, so no information outside that neighbourhood is used. $\square$

The subtraction by one matters: the first of the $r$ edges leaves the new top, leaving only $r-1$ old edges after the descriptor endpoint.

3. Exact readable-cone radius

Define

$$R_{k,h}= \begin{cases} 0,&h=0\text{ or }k=0,\\ k+(h-1)(k-1),&h\ge1\text{ and }k\ge1. \end{cases}$$

Finite-horizon readable-cone theorem. If two cut configurations have the same finite control state and the same radius-$R_{k,h}$ unfolded neighbourhood at their tops, then they give the same accept/reject answer to every continuation of length at most $h$.

Proof. Induct on $h$. For $h=0$, acceptance depends only on the current state. For $h\ge1$, equality at radius $R_{k,h}\ge k$ makes the first transition identical. If another $h-1$ symbols remain, the induction hypothesis asks for equality of the new tops at radius $R_{k,h-1}$. The pullback lemma requires old radius

$$k+R_{k,h-1}-1=R_{k,h}.$$

Thus the new configurations satisfy the induction hypothesis. The case $k=0$ never inspects a port and is immediate. $\square$

This is a uniform future-family statement. The execution-specific causal support of FPRD-T133 may be much smaller after one continuation is fixed.

4. The radius is sharp

For every $k,h\ge1$, radius $R_{k,h}-1$ does not suffice uniformly.

Use a degree-one old scaffold whose unique port forms a backward chain. Put one bit at depth $R_{k,h}$, and give every shallower node the same label. The two bit choices have identical radius-$(R_{k,h}-1)$ neighbourhoods.

On each of the first $h-1$ query symbols, append a node whose port is the descriptor $0^k$. On the last query symbol, inspect the label reached by $0^k$ and accept exactly when it is one. The inspected old depth follows

$$k,\quad 2k-1,\quad 3k-2,\quad\ldots,\quad k+(h-1)(k-1).$$

Hence the two old chains receive different answers after exactly $h$ symbols. They can be produced by ordinary input prefixes: the first data symbol stores the bit and later data symbols extend the chain using the empty old-top descriptor.

5. Counting view types

Let $g=|\Gamma|$. Include the distinguished unlabelled value used by the initial scaffold. Let $V_r$ be the number of abstract radius-$r$ unfolded views when a missing node is also allowed. Then

$$V_0=g+1, \qquad V_{r+1}=1+(g+1)V_r^d.$$

At radius zero, a missing node and an unlabelled node have the same observation. At positive radius, one abstract view is missing; every nonmissing view chooses one of $g+1$ labels and one radius-$r$ child view at each of $d$ ordered ports.

Finite-horizon response-capacity corollary. Across any family of cut prefixes, and for any continuation family contained in $\Sigma^{\le h}$, the number of distinct accept/reject response rows of $\mathcal A$ is at most

$$|Q|V_{R_{k,h}}.$$

Therefore its cut-response dimension is at most

$$\log_2|Q|+\log_2 V_{R_{k,h}}.$$

Proof. The readable-cone theorem says that the pair consisting of the current control state and radius-$R_{k,h}$ view determines the entire response row. Count those pairs and apply FPRD-T152. $\square$

The bound deliberately counts abstract unfolded views, including some that may not be reachable in one particular automaton. It is a uniform capacity ceiling, not an exact reachable-state count.

6. What the theorem does and does not prove

This is the missing capacity half of FPRD-T152 for one fixed scaffolding-automaton parameter tuple. It is insensitive to how much old graph exists outside the readable cone and to physical aliasing hidden by the unfolded observation semantics.

It yields a reusable lower-bound template. To refute a proposed automaton with parameters $(d,k,g,|Q|)$, construct a finite cut and horizon $h$ with more than $|Q|V_{R_{k,h}}$ response rows.

It does not separate a language from all scaffolding automata or all PEGs by itself. Another automaton may use larger fixed degree, distance, alphabet, or finite control. Nor does it bound total archived memory, which remains unbounded with prefix length.

The unary selector is consistent with the theorem. Its query horizon grows with the selected depth, so its readable cone is allowed to grow far enough to reach the retained bit.

FPRD-T69 gives a different exact fixed-cut tradeoff for supplied track layouts and snapshots. The present theorem works directly with the native Loff–Moreira–Reis neighbourhood semantics and gives one uniform bound for all histories of a fixed automaton.

7. Exact audit

The checker enumerates all binary-labelled backward scaffolds in two finite domains:

• degree one on five old nodes, through distance and requested new radius three;
• degree two on four old nodes, through distance and requested new radius two.

Across 13,056 old scaffolds and 4,253,184 possible one-step extensions, every pair with the same radius-$(k+r-1)$ old view has the same radius-$r$ new view. This produces 67,922 same-view signature comparisons.

Separately, 24 chain witnesses cover every $1\le k\le4$ and $1\le h\le6$. In every case the two chains agree through radius $R_{k,h}-1$ and the length-$h$ continuation separates them. The checker also verifies the view-count recurrence on 36 parameter/radius cases.

The computation tests the structural seams and sharpness examples. The induction above proves the unbounded theorem.

8. Source

Bruno Loff, Nelma Moreira, and Rogério Reis, The computational power of parsing expression grammars, arXiv:1902.08272, Definitions 10–13. Their paper introduces scaffolding automata and proves their equivalence with PEGs. The horizon-capacity theorem above is an FPRD synthesis built on that published model. No external or specialist review is recorded for this synthesis.