Segmented transport for repeated filtering

30 September 2026. Written invariant and conditional construction theorem, with finite executable comparison against the abstract scheduler. This note solves the overlap geometry in the forward filtering fragment. It does not yet supply a certified bounded-record catenable sequence or promised undo.

1. The overlap problem has a segment form

Let P keep positions 1, 3, 5, and so on. For a current word w, write

$$w_k=P^k(w).$$

The one-carry scheduler from the preceding note updates these levels in increasing depth. Later appends can begin newer shallow carries before an older deep carry finishes. A FIFO cannot express the resulting order. If an old job has prepared depths 1, 2, and 3 and a new job replaces only depths 1 and 2, the visible order must be

$$\mathsf{new}_1,\ \mathsf{new}_2,\ \mathsf{old}_3.$$

Treating each job as a nested prefix overlay creates a false difficulty: every P appears to require advancing every hidden overlay. The correct coordinates are the gaps between pending carries.

Store the tower as alternating exact segments and carry markers:

$$E_0\ M_1\ E_1\ M_2\ \cdots\ M_m\ E_m\ T. \tag{1}$$

Each E_i is a finite sequence of already materialized level summaries. Each M_i=(u_i,x_i) says that symbol x_i still has to be appended to the old summary u_i at that depth. T is one of the fixed empty or singleton tails. The first marker is the shallowest pending carry.

A global depth shift removes one item only from E_0. The lengths of all gaps between markers are unchanged. This is the key alignment fact.

2. Only finite level summaries are needed

For the target observation, an exact level word need not be stored. Define

$$h(\epsilon)=\mathsf{Empty},\qquad h(v)=(\mathsf{first}(v),\ |v|\bmod 2,\ |v|_a\bmod 2) \quad(v\ne\epsilon). \tag{2}$$

This is a finite set. From h(v) and x one can compute h(vx). The append propagates to the next filtered level exactly when v is nonempty and has even length. The observed answer is the last component. The first component identifies the eventual singleton tail.

Thus every element carried by a segment is finite data. The unbounded memory lies only in the number and linkage of records, not in a record label.

3. The segment transitions

Assume an abstract fully persistent catenable sequence with empty, is_empty, front, pop_front, push_back, and concat. All are required to have worst-case bounded work. Sequence elements range over the finite set of summaries in (2).

Before each external request, service the first marker, if one exists. Put v=append(u_1,x_1).

1. If the carry propagates, E_1 is nonempty. Append v to E_0, remove the first old summary z from E_1, and replace M_1 by (z,x_1).
2. If the carry stops, remove M_1 and replace the neighboring segments by concat(push_back(E_0,v),E_1).
3. If u_1 is empty, the new level and all deeper levels are the fixed singleton tail for x_1; reachable states have no older marker below it.

The no-collision clause in the forward deadline lemma proves the promise in case 1: if E_1 were empty, the next deeper position would already contain M_2, and propagation would create two carries at one level.

After service, an external append updates the finite level-0 summary. If it starts a carry, the exact summary at depth 1 is removed from the front of E_0 and becomes a new first marker, preceded by an empty segment. A P request removes the first exact summary from E_0 and makes it the new level-0 summary. The deadline lemma guarantees that no marker occupies depth 1 at this point. No deeper frame changes.

The smallest overlap now has the literal form

$$[\mathsf{old}_1,\mathsf{old}_2,\mathsf{old}_3] \longrightarrow []\ M\ [\mathsf{old}_2,\mathsf{old}_3] \longrightarrow [\mathsf{new}_1]\ M\ [\mathsf{old}_3] \longrightarrow [\mathsf{new}_1,\mathsf{new}_2,\mathsf{old}_3].$$

Three shifts therefore expose exactly new-1, new-2, and old-3.

4. Segment-dominance theorem

Consider the forward interface {+a,+b,P} from the empty word. Service one shallowest carry before each external request, as in the forward deadline lemma. Initialization uses one empty level-0 summary and the virtual empty tower tail.

Theorem 1 (segmented transport). After every finite forward trace, the alternating representation (1) satisfies all of the following.

1. Reading each segment in order and inserting the old summary stored in each marker yields exactly the scheduler’s materialized summary tower.
2. Marker order and payloads are exactly the scheduler’s pending carries.
3. E_0 contains precisely the exact levels before the shallowest carry.
4. Every service step changes only E_0, M_1, E_1, and a constant number of frame records.
5. Every P step changes only level 0 and the front of E_0.

The theorem includes every reachable nesting depth. It preserves the parity observation of the fixed filtering controller on the same request trace.

Proof

The claim is by induction on service steps and external requests. Initially, there are no markers and the empty virtual tail is the exact tower.

For service, the scheduler either propagates or stops its shallowest carry. In the propagation case, moving the first element of E_1 into the marker position and appending the newly computed summary to E_0 leaves the concatenated materialized tower exactly equal to the scheduler’s update. The no-collision invariant supplies the required first element of E_1. In the stopping case, deleting the marker and concatenating its two neighboring exact segments gives the same tower. The empty case enters a virtual singleton tail. In every case the remaining markers keep their order and payloads.

After service, an append can introduce only a depth-1 carry. Splitting the first exact summary from E_0 creates exactly that first marker. For P, the deadline lemma says depth 1 is exact, so deleting the first item of E_0 promotes the correct summary. Every deeper marker depth decreases by one, but every difference between consecutive marker depths is unchanged. Hence no deeper segment or marker must be rewritten. This proves all five clauses. $\square$

The proof is an abstract invariant proof, not a proof-assistant formalization.

5. Conditional bounded-record consequence

Fix a catenable-sequence implementation C for a finite element alphabet. Suppose each operation of C is realized by immutable finite-tagged records with fixed roots, arity at most q_C, old-access radius at most r_C, and at most A_C fresh records. Require exact sequence semantics on every branch from every older version. Forbid mutation, memoization, address arithmetic, pointer-identity tests, scans, amortized work, and unbounded scalar fields.

Corollary 2 (conditional forward realization). Under those hypotheses, the forward repeated-filtering controller has a fully persistent bounded-record realization. It preserves a-parity after every finite trace over {+a,+b,P}.

Each controller request invokes at most three catenable-sequence operations and rewrites a constant number of segment frames. Closure of fixed finite transition plans therefore gives computable constants depending only on q_C, r_C, and A_C. For example, direct inlining gives conservative bounds of the form

$$q\le \max(q_C,4),\qquad r\le 3r_C+4,\qquad A\le 3A_C+8. \tag{3}$$

These are construction bounds, not optima. Applying the reviewed simultaneous-record compiler adds one scaffold layer and its usual degree bound. The result preserves this fixed controller’s observations on the same operation traces. It does not preserve physical graph identity, arbitrary future scaffold-context observations, or by itself recognize the language of legal traces. Any later scaffold-to-PEG transfer introduces exactly one reversal.

The catenable-sequence hypothesis is checkable without assuming the filtering conclusion: give finite record constructors, explicit transition cases, source-to-record access and allocation counts, and an independent proof that the operations implement sequence concatenation and front updates on every persistent branch.

Corollary 2 is a sufficient condition, not a characterization. The theorem does not say that every filtering representation contains a catenable deque.

6. Verification scope

The checker stores only the finite summary (2) in the segmented machine and retains exact words in a separate reference model. It compares the alternating segments and markers with the abstract one-carry scheduler after every tested transition. Immutable tuples model branching from old versions.

The recorded run checks all distinct forward states through trace depth 13, 24,885 transitions, 240,000 seeded sequential transitions, and 250,000 operations branching among up to 5,000 retained versions. The largest tested state had two simultaneous markers. This does not prove that two is a global bound, and the theorem does not use such a bound.

Python tuple concatenation is not constant-time and is used only as the abstract concat oracle. The finite run therefore corroborates the segment invariant but does not discharge Corollary 2’s record-level hypothesis.

7. Literature boundary and the remaining certificate

Kaplan and Tarjan’s Purely Functional, Real-Time Deques with Catenation establishes immutable catenable deques with worst-case constant-time end and concatenation operations. Viennot, Wendling, Gueneau, and Pottier’s Verified Purely Functional Catenable Real-Time Deques provides a purely functional OCaml implementation and a machine-checked Rocq correctness development. Their paper reports that the OCaml operations are nonrecursive and worst-case constant time. The accompanying VerifiedCatenableDeque repository contains the implementations and verified signatures.

Those results make Corollary 2 credible, but they do not yet discharge its exact model contract. The authors explicitly state that there is no formal connection between the hand-written OCaml implementation and the verified Rocq implementation. The efficient public OCaml wrapper stores an exact integer length, and the core buffer code performs size tests. The extracted verified code retains natural-number indices and is not constant time. An exact FPRD import must therefore erase or structurally replace those scalars, audit every reachable constructor and helper call, and derive concrete old radius and allocation bounds.

The simpler Kaplan-Okasaki-Tarjan catenable deque is not a substitute: the recent Verified Persistent Catenable Deques confirms that it uses restricted mutation and gives a worst-case amortized, not strict worst-case, bound.

The established ingredients are the carry deadline lemma and real-time catenable deques. The additional argument here is the alternating-segment factorization that turns all overlapping filtering repairs and all common depth shifts into a constant number of catenable-sequence operations. Novelty of that reduction has not been established.

8. Exact next question

Audit the efficient Kaplan-Tarjan catenable-deque source against the FPRD record model. Either produce a scalar-free finite-constructor certificate with explicit radius and allocation bounds, or isolate the first operation that cannot be made structural. A successful certificate completes the forward fragment by Corollary 2. Only then should promised typed undo be added.

The failure of a particular catenable-deque presentation would not refute all bounded-record filtering representations.