The real-time frontier for persistent filtering

30 September 2026. Written finite-horizon proofs with an executable adversarial explorer. This note does not prove a bounded-local persistent realization of the full interface. It isolates the remaining obstruction after a natural allocation argument fails.

The current test problem stores a binary word w. Appending and correctly specified last-symbol undo are permitted. A filtering request P keeps positions 1, 3, 5, and so on, counted from the left. The observed output is the parity of the a symbols. The goal is a fixed finite rule set with bounded local pointer access and bounded immutable allocation per request.

The preceding finite-summary result proves that no fixed finite state can support arbitrary repetitions of P. That does not settle the persistent problem. A growing representation has enough total space to retain a hierarchy of progressively filtered words. The difficulty is maintaining that hierarchy in worst-case constant work.

This note establishes two facts:

1. an eager hierarchy with explicit ready-to-follow filter links has an unbounded single-update allocation cost; but
2. the cascade has a real-time schedule in the forward fragment containing append and P: one pending carry step per request always prepares the level that the next P can expose.

Thus neither the finite-summary obstruction nor the apparent binary carry is a representation-independent lower bound. The open problem is now the immutable pointer-local realization of the schedule, with persistent undo.

1. The dyadic tower

For k>=0, put

$$w_k=P^k(w),\qquad n_k=|w_k|, \qquad b_k=|w_k|_a\pmod 2. \tag{1}$$

The tower shifts under filtering: the tower of P(w) is (w_1,w_2,...). For a new symbol x, the symbol survives at level k exactly when its new position is congruent to 1 modulo 2^k. Thus, for n=|w|>0,

$$w_k(wx)= \begin{cases} w_k(w)x,&2^k\mid n,\\ w_k(w),&2^k\nmid n. \end{cases} \tag{2}$$

The first symbol is a special finite base case: every nonempty level beyond the word’s height is the same singleton. Two fixed virtual singleton records, one for each symbol, can represent these infinite constant tails.

Equation (2) is a binary carry. An append after a word of length divisible by a large power of two changes many consecutive tower levels.

2. Why the eager filter-link layout is not real time

Define an exact eager tower layout to have one immutable record for every nonconstant tower level. A record represents that level’s exact word version, contains its finite aggregate label, and has a distinguished pointer to the record for the next filtered level. A P request merely follows that pointer; it performs no rebuilding. Different exact words of different lengths cannot be represented by the same record. Fixed singleton tails may use virtual records.

Proposition 1. No exact eager tower layout has a uniform allocation bound for append.

Proof. Let w=b^(2^j) and append a. For every 0<=k<=j, the new a occupies position 2^(j-k)+1 in P^k(wa), so

$$P^k(wa)=b^{2^{j-k}}a.$$

Before the append the corresponding word is b^(2^(j-k)). These j+1 exact tower levels all change, have different lengths, and must be represented by j+1 new immutable records linked in order. At level j+1, the new symbol is discarded and the old singleton suffix can be reused. Since j is arbitrary, no fixed allocation bound exists. ∎

This is a restriction on one presentation, not on every representation of the interface. In particular, it assumes that every filter link is already materialized and that the stored levels are exact words rather than behavioral summaries or suspended computations.

3. A one-step cascade schedule

The eager proof suggests doing the changed levels gradually. A materialized append of x at level k creates a carry to level k+1 precisely when the old positive length at level k was even. The carry says: append x at the next level. Processing that carry can create one carry a level deeper. Appending to an empty level instead enters the fixed singleton tail and creates no unbounded cascade.

Use the following abstract scheduler for the forward interface {+a,+b,P}:

1. before every external request, process the shallowest pending carry, if there is one;
2. perform the requested append at level 0, possibly leaving a carry at level 1; or
3. for P, promote level 1 to level 0 after the preliminary carry step.

The scheduler stores at most one pending symbol per level. A carry’s level is part of this abstract description; Section 5 explains why representing that priority locally is not free.

Theorem 2 (forward deadline lemma). Starting from the empty tower, the abstract scheduler has the following properties after every finite sequence over {+a,+b,P}:

1. level 0 is the exact current word;
2. every level before the shallowest pending carry is exact;
3. there is at most one pending carry at each level; and
4. after the preliminary carry step of a P request, level 1 is exact, so promotion is always correct.

Only one carry is processed per external request. A carry step reads one level state, appends one finite symbol, and produces at most one deeper carry.

Proof

The claim is by induction over external requests and processed carries. A carry at level k is created only by an append at level k-1 whose old positive length was even. The resulting length at level k-1 is odd. Before another carry to level k can be created, that level must first receive an intervening append changing odd length to even; that intervening append creates no carry to k.

The scheduler always processes a shallower carry before a deeper one. During the intervening request just described, either a new shallower carry is being processed, or the old level-k carry is the shallowest and is removed. Hence a second level-k carry is never added while the first remains. This proves property 3.

An external append changes level 0 immediately, so property 1 is preserved. It can add only a level-1 carry. All levels shallower than the first pending carry have already received every append that survives to them, proving property 2.

Before P, if level 1 has a carry, it is the shallowest and the preliminary step processes it. If it has none, property 2 already says level 1 is exact. Promotion is therefore correct. Shifting the tower and all remaining carry levels down by one preserves the order and uniqueness of carries. The fixed empty and singleton tails establish the base cases. ∎

The theorem is stronger than an amortized count. The eager append at a power-of-two boundary may expose an arbitrarily long cascade, but later filtering can reveal only one new level per request. The scheduler meets those deadlines one step at a time. A claimed lower bound based only on the number of changed dyadic levels is therefore false.

4. Exact verification scope

The checker explores every distinct abstract scheduler state reached by all forward traces through the recorded depth and additional seeded random traces. It retains the raw current word and every materialized tower word through a finite cutoff. It verifies:

• level 0 equals the raw word;
• a level is exact whenever no shallower pending carry can affect it;
• no level contains two pending carries;
• every promotion is exact after one preliminary carry step; and
• the eager family b^(2^j)a changes exactly j+1 nonconstant levels through the recorded range.

The finite exploration corroborates Theorem 2 and Proposition 1 but proves neither unbounded statement. Their proofs are the written arguments above. The checker does not implement pointer-local task storage, persistent undo, a scaffold, or a proof assistant formalization.

5. Why this is not yet the desired construction

The abstract scheduler names the shallowest pending level and updates its materialized state in one step. The target record model offers no array index, unbounded level number, pointer-identity branch, or mutable cell. Its fixed roots may inspect only a bounded old neighborhood and may allocate only a bounded fresh batch.

A valid implementation must therefore represent four relationships locally:

1. the current level and the next level that P may promote;
2. the shallowest pending carry and its target level;
3. the continuation needed to reconnect a rebuilt deeper level; and
4. for every materialized append, a predecessor version that typed undo can restore.

Naively storing the tower as a linked list makes a deep scheduled update nonlocal. Storing a direct pointer to the job makes the job local but does not by itself reconnect its updated result to the tower head. A zipper can retain the path, but rebuilding all ancestors at once repeats the eager allocation problem. A real-time continuation must rebuild that path incrementally while still allowing P, append and rollback to operate on the exposed version.

Persistent undo is not dismissed as a routine addition. A materialized append can point to its predecessor tower version, so undo itself can be one pointer step. But background work performed after that append may be abandoned when undo restores the predecessor. The proof must show that every restored schedule still meets future deadlines without relying on work done only in the discarded version. The forward deadline lemma does not prove that pointer invariant.

6. Relation to established data-structure theory

Driscoll, Sarnak, Sleator and Tarjan’s Making Data Structures Persistent formalizes linked structures with fixed fields and fixed entry pointers. Its generic node-copying transformations assume bounded in-degree and primarily give amortized update-space bounds. Our target is write-once, has a stricter bounded-local observation rule, and asks for worst-case bounded allocation; their theorem cannot simply be invoked as the missing compiler.

Okasaki’s Purely Functional Data Structures explains both relevant phenomena: persistence invalidates naive amortization, while premature scheduling can convert incremental lazy work into real-time operations. His real-time queues force a fixed amount of a schedule per operation. The published implementations use lazy streams and memoization; our immutable record model must represent any suspension, completed result and version rollback explicitly. The scheduling idea is established, but the filter-tower invariant and its compilation are not imported from that work.

Recent verified catenable real-time deques confirm that sophisticated purely functional worst-case scheduling is possible, but deque operations do not include this dyadic filtering transformation. Literature comparison has not established novelty of Theorem 2, and an unsuccessful search would not do so.

7. Next decisive question

The immediate problem is no longer whether there is enough total work. It is:

Can the one-carry forward scheduler be represented by a fixed-root, immutable continuation zipper with bounded old access and bounded fresh allocation, while every restored predecessor version retains the deadline invariant?

The next proof attempt should specify the actual record types and transition table for the smallest useful case. It should first cover {+a,+b,P} and only then add typed undo. A forward construction is substantive but not the full theorem. If a zipper layout fails, retain the precise access or allocation witness; do not generalize that failure to every pointer representation.

Conversely, a lower bound must quantify over all finite labels, controls, fixed roots, bounded arities, bounded old-access radii and bounded allocations in the stated model. Proposition 1 does not meet that standard.

No language-recognition result follows yet. A completed source-to-scaffold construction would preserve the chosen completed controller on the same input words; the PEG transfer would introduce exactly one reversal. Promised typed undo would still require a separate validator before claiming recognition of exactly the legal trace language.