When propagation is hard and replay is enough

4 October 2026. Research note. Written constructions and reductions, independently reviewed; the data-structure lower bounds are imported.

The dynamics of a constraint problem include when its information becomes available. A gate can be easy to evaluate when its inputs are already known, yet a large collection of gates can be difficult to prepare for values and a query that arrive later. Native scaffolding automata make that distinction precise because every input symbol supplies one computation step and the answer is due at input end.

Three results sharpen this distinction. Arbitrary-order implication constraints with two late pins already resist native recognition, unconditionally. More generally, the graph relation of every Boolean function depending on at least two inputs, together with pins, gives a nonrecognizable constraint language. In the other direction, ordered circuits whose inputs are available before use have native recognizers. For a precisely defined ordered XOR-circuit language that allows late inputs, one pass is impossible but one verified replay is sufficient.

These also give expressive-power statements about parsing expression grammars. In particular, we exhibit an explicit language $L$ such that

$$L\notin\mathsf{PEG},\qquad \{w\mathbin{\#}w:w\in L\}\in\mathsf{PEG}.$$

The second language requires the two copies to agree; their equality is checked by the recognizer. The copy adds computation time and another traversal of the same information.

The common encoding and machine contract

Use a fixed finite alphabet of relation tags and punctuation. A record has a tag, parentheses, comma-separated nonempty binary variable names, and a semicolon. For example, I(1,10);T(1);F(10); asserts $x_1\Rightarrow x_{10}$ and pins its endpoints to true and false. Names are literal words: leading zeros and prefix relationships matter. Repetition and arbitrary record order are permitted for ordinary constraint satisfiability. The empty conjunction accepts and malformed strings reject. Every character counts toward encoded length $N$; $b$ denotes the number of distinct variables.

A native deterministic scaffolding automaton has fixed finite control, labels, degree, observation radius and initialization, independent of $N$. Each arriving symbol creates one immutable node. The transition observes the bounded labelled port unfolding from the old top and routes new edges along bounded port paths. It cannot compare physical pointer identities, inspect numerical addresses, mutate old nodes, or compute after input end. There are $N+1$ physical nodes, with $O(N\log(N+2))$ bits under literal pointer encoding.

The native model and PEG equivalence, Definitions 10–15 and Theorem 16 of Loff–Moreira–Reis, give

$$A\in\mathsf{SA}\quad\Longleftrightarrow\quad A^R\in\mathsf{PEG}.$$

We track this reversal explicitly. Ordinary implication and gate-constraint exclusions below hold in both orientations. The ordered circuit and replay constructions are forward-orientation statements; their PEG consequences use the reversed languages.

Directed propagation already crosses the boundary

Let $I(x,y)$ mean $\neg x\lor y$, and let $T,F$ be the two unary pins.

Propagation theorem. Ordinary $\operatorname{SAT}_{\rm enc}(\{I,T,F\})$ and its reversal are outside native SA. The hard formulas can have an acyclic implication graph, followed by just one true pin and one false pin. Direct signed-clause encodings give the same exclusion for ordinary Horn-SAT and 2SAT.

The logical mechanism is familiar. A prefix

$$I(x_1,x_2)\land I(x_2,x_3)$$

becomes inconsistent after $T(x_1)\land F(x_3)$. For a general directed graph $G$, write

$$F_G=\bigwedge_{(u,v)\in E(G)} I(x_u,x_v).$$

Then

$$s\leadsto_G t \quad\Longleftrightarrow\quad F_G\land T(x_s)\land F(x_t)\text{ is inconsistent}.$$

A path propagates truth from $s$ to $t$. Conversely, if no such path exists, set exactly the vertices reachable from $s$ to true. Every implication and both pins are satisfied. Every implication-only prefix has a satisfying all-zero assignment.

The imported lower bound and the exact translation

Larsen–Yu prove that insertion-only reachability in an $n$-vertex directed acyclic graph, with worst-case update cost $t_u$, expected query cost $t_q$ and $w$-bit cells, satisfies

$$t_q=\Omega\!\left(\frac{\log^{3/2}n}{\log^2(t_uw)}\right),\qquad w=\Omega(\log n).$$

See Theorem 1, printed p1, the fully adaptive cell-probe model in §1.1 p2, and the insertion-only reduction in §4 pp8–10. Lemma 5 in §5.1 uses a final query after all update epochs. These are precisely the operations used here; no deletion, semi-adaptive access order or earlier query is required.

Suppose one fixed native recognizer existed. Give graph vertices distinct $d$-bit names, $d=\lceil\log_2(n+1)\rceil$. Process an edge insertion by appending its I record. Answer a reachability query by simulating the two pin records and negating acceptance.

For $m$ distinct inserted edges, the complete ordinary word has

$$N=m(2d+5)+2(d+4),\qquad b\le n.$$

The hard workload has $m\le n(n-1)/2$. Store each native node in a constant number of logarithmic cells. Fixed degree and radius mean a transition uses $O(1)$ probes. Store the top, finite control and allocation counter in charged cells as well. Hence

$$t_u=O(\log n),\qquad t_q=O(\log n),\qquad S=O(N)\text{ words},\quad w=\Theta(\log n).$$

All allocated history is included; sufficiently large constant word width accommodates its addresses. Initial storage is constant and independent of $G$. There is no free graph preparation, external name handle, future-input knowledge or deferred terminal work.

The source requires read-only queries. New native nodes created while processing the query suffix can instead be represented inside that query’s transient computation. Reading an old node still incurs a probe; the transient nodes and control are discarded after the answer. They do not become a free persistent cache. Thus this is a legal adaptive query decision tree.

The imported lower bound would require

$$t_q=\Omega\!\left(\frac{\log^{3/2}n}{(\log\log n)^2}\right)=\omega(\log n),$$

a contradiction. This excludes every native representation, not merely a proposed propagation algorithm.

For the reverse-language claim, feed the reversal of each individual record as its edge or pin arrives. Reversing the completed string gives the original records in reverse order. Conjunction is order-independent, so the same equivalence and budgets hold. For Horn-SAT and 2SAT, use signed-clause records C(-u,+v);, C(+s);, C(-t);, where the names replacing $u,v,s,t$ are written literally and 2CNF permits at most two literals per clause. These encode $(\neg x_u\lor x_v)$ and the two units; their lengths remain $O(\log n)$. No general closure under SAT reductions is assumed. Theorem 16 then excludes both PEG orientations too.

Every genuinely combining Boolean gate is enough

Fix a total Boolean function $f:\{0,1\}^k\to\{0,1\}$, with fixed $k$, and its graph relation

$$G_f(x_1,\ldots,x_k,z)\quad\Longleftrightarrow\quad z=f(x_1,\ldots,x_k).$$

An input is essential if changing it can change the output while the other inputs stay fixed.

Gate theorem. If $f$ has at least two essential inputs, ordinary satisfiability over $G_f,T,F$ has no native SA or PEG in either orientation.

Here formulas are arbitrary conjunctions of gate-relation records. No single-assignment syntax or evaluation order is assumed. This contract differs from the ordered circuit controls below.

Affine gates

If $f=c\oplus\bigoplus_{i\in J}x_i$, its graph is the equation

$$z\oplus\bigoplus_{i\in J}x_i=c.$$

At least two essential inputs give support at least three. Pinning all but two selected inputs produces a ternary parity relation. The unconditional affine obstruction, importing Ko’s fully adaptive inner-product theorem, applies. Its even/odd parity conversion and ordinary-name budgets are unchanged.

Nonaffine gates

The algebraic normal form of a nonaffine Boolean function contains a monomial of degree at least two. Choose two coordinates $i,j$ in such a monomial. The mixed Boolean derivative $\partial_i\partial_jf$ is nonzero: deleting $i,j$ from distinct monomials containing both leaves distinct monomials. A nonzero multilinear polynomial is nonzero on some Boolean assignment. Fix all other coordinates to such an assignment. The resulting binary restriction is

$$g(x,y)=xy\oplus bx\oplus cy\oplus d.$$

Pins implement those fixed coordinates. Six of the eight possibilities give implication by projecting one input out of the graph:

Swapping the endpoint names handles the transposed implications. The remaining NAND and NOR gates also implement $I(a,b)$:

$$\begin{aligned} I(a,b)&\Longleftrightarrow \exists h,c\ [T(c)\land G_{\rm NAND}(b,c,h)\land G_{\rm NAND}(a,h,c)],\\ I(a,b)&\Longleftrightarrow \exists h,c\ [F(c)\land G_{\rm NOR}(a,c,h)\land G_{\rm NOR}(h,b,c)]. \end{aligned}$$

In the first formula $h=\neg b$, and the other gate requires $\neg(a\land\neg b)=1$. In the second $h=\neg a$, and the other gate requires $(\neg a)\lor b=1$.

To apply the propagation lower bound, expand each arriving graph edge into its fixed gadget. Give private variables fresh names indexed by the edge occurrence and a fixed slot. With at most polynomially many edges, these names have $O(\log n)$ symbols. Use fresh pinned constants inside each edge gadget, so their initialization is charged too. Each update still appends $O(\log n)$ characters; the final two pins retain that budget. Private witnesses exist independently exactly when all endpoint implications hold. The number of variables is $O(n+m)$ and encoded length is $O((m+1)\log(n+2))$ for the hard workloads. All storage remains polynomial. This direct simulation uses no general inverse closure under existential gadget substitutions.

Constant-output gates are Cartesian unary constraints and have native recognizers. A one-essential-input gate is equality or disequality, with possible irrelevant arguments; their native membership remains unresolved. The theorem establishes a structural obstruction, not a completed positive classification.

A NAND gate graph is different from the binary NAND clause relation. The former is covered unconditionally above; the pure latter family with pins retains its OMv-conditional obstruction. Adding disequality to NAND or OR does implement implication, so those mixed languages are excluded unconditionally as well.

Ordered circuits: availability before use gives a positive case

Now orient each gate record as an assignment to its final argument. For any fixed finite collection of Boolean gates, define a circuit language with the following checked conditions: each output has only one producer; every operand is either an earlier output or a variable never produced by a gate; these source variables are pinned before their first use; all pins on every variable are mutually consistent, including names used only in pins; and pins on computed outputs agree with their values. Pins and gates may otherwise interleave. This is an explicitly restricted presentation, not an implicit ordering promise for ordinary SAT.

Availability theorem. This language has a native SA recognizer.

The key tool is the serial binary-name dictionary. Its proof permits any fixed finite payload, not just a set of permitted unary values. Its path frames preserve a terminal payload and two subtrees. Replacing the terminal payload by a finite function of the old payload and controller state preserves the same path-fold and explicit-tip invariants. Monotonicity of unary intersections was needed only for interpreting the earlier application, not for the dictionary operations.

Store a pin mask, a produced bit, a computed value, and a bit recording whether the variable has been used as an unproduced source. At an operand name, use its computed value if produced; otherwise require a singleton current pin mask and mark it as used as a source. At the output name, reject a duplicate producer or a previously used source, compute the fixed gate from the finitely many saved operand bits, and check its pin mask. A pin intersects its mask and also checks an already computed value.

The source-use bit matters: an early pin cannot disguise a future producer as an available source. Its later definition is rejected. Self-reference, forward dependencies, duplicate producers, contradictory late pins, and prefix-related names are therefore all checked. Induction over complete gate records proves exact evaluation. Every name is processed bit by bit; its closing delimiter commits the finite payload update. At a comma, the same bounded batch resets the current subtree to the committed root and empties the temporary path FIFO for the next name. The final acceptance test requires only finite control, with no scan after input end.

The dictionary has fixed work, observation radius and fresh allocation per symbol. Adding finite payload fields and a fixed gate’s operand bits preserves those bounds. The reviewed simultaneous-record compiler yields one fixed native automaton. All source history is $O(N)$ records; literal pointer storage is $O(N\log(N+2))$ bits.

Late inputs: one verified replay changes the answer

Define $K$ using only X(u,v,t);, meaning $t:=u\oplus v$, and the two pins. Require single assignment and require every operand to be an earlier gate output or a nongate source pinned somewhere in the complete word. All pins on every variable must be mutually consistent, including pin-only names, and pins on outputs must agree with the resulting evaluation. Source pins may now arrive after their uses. Malformed words and failed order conditions reject; the empty word accepts. Repeated operands are allowed, while self-reference is not.

For example, X(1,10,11);T(1);F(10);T(11); is valid: the source values arrive after their gate, and the output assertion agrees. The definitions and validity conditions are part of the language, not unchecked advice.

Replay theorem.

$$K\notin\mathsf{SA},\qquad D_K:=\{w\mathbin{\#}w:w\in K\}\in\mathsf{SA}.$$

Why the first pass alone cannot suffice

The parity reduction already has exactly this circuit form. For $m=n^2$ matrix rows, write $F(z)$ and row-major gates

$$a_{ij}:=a_{i,j-1}\oplus t_{ij},\qquad a_{i0}=z,\quad t_{ij}=\begin{cases}x_j&M_{ij}=1,\\z&M_{ij}=0.\end{cases}$$

All producers are distinct and every dependency on a producer points backward. Afterwards, pin every $x_j$ to the arriving vector coordinate and finish with one $F(a_{in})$ query. The word belongs to $K$ exactly when that row’s inner product is zero. It has $b=1+n+mn$ variables and, for $d=\lceil\log_2(b+1)\rceil$,

$$N=(d+4)+mn(3d+6)+(n+1)(d+4)=\Theta(n^3\log n).$$

Ko’s Theorem 1.1, full statement in §3 p12 and Protocol 4 pp14–16 excludes polynomial preparation with polylogarithmic coordinate updates and a query using $o((\log n/\log\log n)^2)$ probes. A native recognizer would again supply $O(\log n)$ updates and query. The saved proof’s charged registers, storage and ephemeral query construction apply unchanged. Incomplete preparation prefixes need not themselves belong to $K$.

A complete native recognizer for the verified replay

During the first copy, enqueue each character in a strict persistent FIFO. In the finite-payload dictionary collect each variable’s pin mask and whether it is a gate output. Reject duplicate producers and conflicting pins. No gates are evaluated yet. At #, require a complete record boundary and switch the finite controller to the second phase.

For each second-phase character, compare it with the copy FIFO’s front and dequeue once. A mismatch or empty queue rejects. Simultaneously parse the replay and evaluate its gates. A gate operand marked as a producer must already have a computed value; an operand not marked as a producer must have a singleton pin mask. At the output, store the XOR and compare it with the pin mask. All pins are now known, including those appearing late in the first copy.

The first phase checks producer uniqueness and pin consistency. Induction over the second phase’s gates checks the dependency order, source assignments and output assertions. The queue enforces literal equality of the copies, including punctuation and name spelling. A short copy leaves a nonempty queue; an extra character underflows it. A missing or additional separator rejects. The input # accepts the empty circuit.

After every symbol the controller knows the parser status, queue emptiness and rejection flag. Consequently ordinary final-state acceptance checks exactly that the replay is complete, with no terminal computation.

The dictionary and copy FIFO are separate bounded local structures. Their headers fit in one fixed-arity record; only one copy enqueue or dequeue occurs per symbol. The saved dictionary/FIFO bounds admit the conservative simultaneous-batch certificate $q=6$, $A=64$, $r=24$ with one root. The reviewed compiler gives fixed native degree at most $385$ and radius at most $25$. These constants certify existence; their optimization plays no role. At target length $L=2N+1$ there are $L+1$ physical nodes, $O(L)$ total logical history and $O(L\log(L+2))$ literal pointer bits. The first pass, stored copy, replay and all discarded versions are charged.

Thus the same ordered gate family has three distinct contracts:

The replay supplies no new assignment information. It gives the automaton a second encounter with each dependency after the relevant metadata and input values are known.

The PEG separation and reduction consequence

Put $L=K^R$. The exact SA/PEG equivalence gives $L\notin\mathsf{PEG}$ and $D_K^R\in\mathsf{PEG}$. Since

$$D_K^R=\{u\mathbin{\#}u:u\in K^R\},$$

this proves the PEG statement at the beginning of the note. This circuit example uses the reversed circuit encoding; the earlier ordinary implication and gate-SAT exclusions cover both orientations separately.

The map $f(w)=w\#w$ can be computed by a deterministic two-way finite-state transducer: copy forward, emit the separator, rewind without output, then copy forward again. It uses linear total time and output, with bounded output per transducer step. Because $f^{-1}(D_K)=K$, native SA languages are not closed under inverse application of this particular map. Linear-size copying is therefore not automatically a recognition-preserving reduction.

Kim–Park’s separation work already establishes reversal nonclosure, which itself rules out general inverse closure under two-way finite-state transductions. The additional content here is the explicit order-preserving copy map and its verified SAT-circuit witness. This does not decide whether any particular smaller gadget substitution is safe.

What remains at the equality boundary

Equality and disequality only identify or invert values along components. They do not implement the combining gates above. Their native recognition remains a consequential unresolved test.

There is now a precise reason the obvious matrix argument cannot simply be reused. For an arbitrary 2-affine prepared formula, positive-pin activation, and a row query independent of the activation, the minimum number of query equations is exactly the number of distinct matrix column patterns selected by that row. A matrix containing an all-ones row and the identity rows forces $n$ query atoms and $\Omega(n\log n)$ query symbols, even with unlimited preparation and auxiliary aliases. The full minimum-query proof closes that interface route while leaving other representations open.

The next native test is current-component access during a streamed variable name: can arbitrary equality merges preserve immediately readable pin information, including overlapping merges and a short final query? The available persistent-union structures do not yet supply that exact immutable, symbol-by-symbol interface. The propagation and replay results give concrete controls against which such a mechanism can be assessed.

Contribution and proof status

Larsen–Yu supplies the directed-reachability lower bound; Ko supplies the inner-product lower bound. Kim–Park supplies the established serialized cell-probe transfer strategy. The positive construction specializes functional-trie and FIFO methods already compared with Demaine–Langerman–Price, using the Lab’s reviewed native compiler and dictionary proof.

The contribution is a set of extensions and applications of those methods: the ordinary implication obstruction, its uniform consequence for genuinely combining Boolean gates, and an explicit one-pass/verified-replay separation with a PEG witness. The functional Boolean restriction argument is elementary; the lower-bound techniques are imported. Independent reviews checked the actual source hypotheses, gadget identities, names, storage, orientations and terminal deadlines. These are written proofs, not proof-assistant verification. A small semantic experiment exercised hostile circuit cases; the inductive construction establishes the unrestricted result.