Ordered suffix maxima with input-paid splicing

10 October 2026. Assessment 196. Written native theorem 63, extending theorem 62. No root admission or external novelty claim.

Current continuation: Persistent length bands remove the final maximum-diversity bound for complete interval rows. The fixed-diversity theorem and its historical next test below remain intact.

Statement and payoff

Written theorem 63. For each fixed positive integer $K$, one fixed deterministic native scaffolding automaton recognizes the ordinary right-first pinned Horn SAT language of the encoding contract, restricted to nonempty final right rows containing exactly all binary words whose lengths lie in an interval $[b_v,H_v]$, with $1\le b_v\le H_v$, and at most $K$ distinct final maxima. The restrictions are checked on ordinary input. Work and allocation are bounded per actual symbol, including the final symbol.

Names, row populations, lower endpoints, intermediate maximum diversity, target order, duplicate records and retained histories are unrestricted. The palette is learned, not supplied. This extends two-maximum suffix reuse to every fixed final maximum diversity. It remains serial reuse after right preparation, not a join of independently supplied stores. The language consequence is a PEG for the reversal of the checked encoding.

The structural criterion is a fixed number of ordered ranges, each with a common upper-validity region. Lower-endpoint work may remain pending while earlier ranges answer. Ordinary names fund each range’s deferred classification and minimum reduction; the range boundary supplies the remaining query time. The number of ranges is fixed, but their endpoints and the represented union are not bounded.

1. Imported sequence primitive and inherited native components

Use the strict, purely functional, worst-case constant-time catenable deque of Kaplan and Tarjan, as extracted in review 195. Only empty, first/last view, removal at an end, insertion at an end and catenation are used. Elements are constant-size pointer records. No ordered comparison, measurement, interior split, laziness or memoization is requested. A public operation performs a bounded number of strict list observations and constructions on available roots. Its finite cases therefore compile with the inherited simultaneous-record compiler. This is an imported data-structure theorem, not a new deque implementation.

Retain the ordinary-name dictionaries, complete-level and interval validators, unary rulers and incrementally prepared binary endpoint numerals from the suffix producer. Retain the current maximum-population histogram and its two-terminal update from input-dominated routing. Retain the strict FIFO and sparse-age minimum worker. Every imported or inherited root is constructed from input or empty initialization; none is supplied as advice.

2. An occupied-depth sequence with ordinary unary gaps

Maintain a catenable deque of entries in increasing occupied histogram depth. An entry contains an absolute ruler/numeral payload and a nonempty ordinary unit stack whose length is the difference from the preceding occupied depth, taking the predecessor of the first entry to be zero. Population is read from the current histogram, not cached in this sequence. In particular, a row stores no purported current bucket handle.

For each actual target word, begin a speculative cursor at depth zero. Keep an empty prefix deque $P$, the old sequence as a suffix, a view of its first entry and its gap cursor, and an empty accumulator $A$. The current-position ruler/numeral and old row maximum ruler are advanced in the inherited lanes. Each target bit does the following bounded work:

1. Reset the retained-at-current-depth flag to false. Advance one depth and prepend a unit to $A$. If a next entry exists, consume one unit of its gap cursor.
2. If that gap becomes empty, the current depth is exactly that entry’s depth. Inspect the same-depth current histogram population. If this is the old row maximum and its population is singleton, omit the entry speculatively. Otherwise append an entry with its old absolute payload and gap $A$ to $P$, set the retained-at-current-depth flag to true, then reset $A$ to empty.
3. Remove the reached entry from the old suffix and expose its next entry and full gap, if any. Do not consume this next gap until the next target bit.

Gaps are positive, so at most one occupied entry is reached per bit. The old maximum is identified by the local termination of its ruler; the zero case has no departure. A finite flag remembers whether an entry was retained at the current depth. Existing endpoint payloads are copied as opaque roots. $A$ is built by actual bits; units need no orientation-sensitive values.

After $n$ bits, $P$ contains precisely the occupied depths at most $n$ after speculative singleton removal, with correct gaps. $A$ measures the distance from its last retained depth (or zero) to $n$. If a next old entry exists, its gap cursor measures the distance from $n$ to that entry; the remainder of the old suffix is untouched. These invariants follow by induction on the three operations above, including omitted entries: omission leaves $A$ accumulating while the next old gap starts at the omitted depth.

At the delimiter, if $n\le h$ for the old row maximum $h$, discard the speculative roots and retain the old sequence. Whether the old ruler has been passed is already a finite flag. Otherwise the existing histogram update changes $h$ to $n$, and:

• If an entry was retained at depth $n$, $P$ already ends at $n$.
• Otherwise append an entry at $n$ using the prepared current-position payload and gap $A$. This gap is positive.
• If an old suffix entry remains, replace only its first entry’s gap with the residual gap cursor. Keep its absolute payload and all later entries. Catenate $P$ with this adjusted suffix. If none remains, use $P$.

The delimiter uses a fixed number of deque operations and records. In the changing case $h<n$, so every possible departure has been visited. Inserting $n$ makes the residual suffix gap exactly correct. No append of unary gaps and no walk to a distant successor is needed. For a new row there is no departure; for an unchanged maximum the speculative sequence is simply ignored.

Splice lemma. After every record, the sequence represents exactly the current occupied histogram depths with correct absolute payloads and gaps. Each target bit and delimiter has bounded local cost, independently of distances, populations and intermediate diversity. The proof is the cursor invariant and the preceding delimiter cases; immutability gives the same statement separately for every retained version.

For the motivating state $\{1,2,M\}$, moving the only row at 1 to 2 visits only depths 1 and 2. The prefix ends at 2; the old entry at $M$ is retained with residual gap $M-2$. The payload at $M$ is already accessible in one deque view. Arbitrarily many intervening empty depths cause no extra delimiter work. Earlier words paid to create that gap and payload.

At the right boundary, retain the existing literal completeness and interval gates and check the occupied-count stack has at most $K$ cells. Take at most $K+1$ front views of the new sequence. On valid nonempty right input this yields ready ordered payloads

$$L_1<\cdots<L_m,\qquad 1\le m\le K.$$

This is a fixed-size export, not a scan of the right rows. Intermediate diversity was never capped. Empty right input is a finite special case.

3. Three maxima: two independently serviced filters

For $m=3$, keep three minimum lanes. Lane zero receives every selected lower endpoint. Lane one receives precisely rows whose maxima differ from $L_1$. Lane two receives precisely rows whose maxima differ from both $L_1$ and $L_2$. Since the frozen palette is exact, these are respectively all rows, rows above $L_1$, and rows above $L_2$.

The two filters run independently. Lane two need not wait for lane one’s backlog: the ordinary-name release supplies the same ready row payload to both fixed queues. Each filter performs sequential linked-digit equality tests against its own finite prefix of the palette. Equality rejects the row; inequality with every tested endpoint releases its lower numeral into that lane’s sparse worker. There is no uncharged transfer of a batch from one filter to another. Each original release reserves both its filter work and possible minimum work.

For query ranges $n\le L_1$, $L_1<n\le L_2$, and $L_2<n\le L_3$, the appropriate lane’s minimum lower endpoint decides membership. An enormous $L_3$ never delays the first two ranges. This parallel organization closes the three-maximum target without assuming that a cascade’s last-stage completion bound would protect earlier ranges.

4. Fixed $K$: original-release credits at each boundary scale

Generalize the preceding receipt to lanes $j=0,\ldots,m-1$. Lane $j>0$ tests equality against $L_1,\ldots,L_j$ and receives exactly selected rows with $H_v>L_j$. Lane zero receives all selected rows immediately. Each lane has its own minimum worker; positive lanes additionally have a strict FIFO and one active comparator. Palette indices and lane counts are finite control for fixed $K$.

During each ordinary intermediate-name bit, service the current receipt. At the delimiter, its first distinct nonempty selection releases the prepared row into all positive filter queues and its lower numeral into lane zero. Missing/repeated selections add no jobs. No preceding name service is credited to the newly released job. The source capsule and deduplication trie are the inherited ones.

A normalized service macro performs one bounded classifier step and one sparse-worker step in every lane. A classifier step starts an operand, reads one pair of linked bits, ends a comparison or releases/discards one row. A terminal comparison step includes setting up the next palette comparison when one remains. Restarting the upper numeral for the next palette endpoint uses its retained root, not a copied numeral. Write $\ell(x)=\lfloor\log_2 x\rfloor+1$ for positive binary numeral length. Equality of arbitrary $H$ to $L_i$ takes at most $\ell(L_i)+2$ steps, even when $H<L_i$: unequal termination stops immediately. Thus all filter work in lane $j$ is at most

$$C_j=\sum_{i=1}^j(\ell(L_i)+2)\le j(\ell(L_j)+2).$$

For an analysis cutoff $k$, reserve at the original release $D_{j,k}=C_j+2k$ credits for this filter and its possible minimum work through the first $k$ ages. The sparse-worker bound charges at most $2k$ to a released lower numeral. Rejection discards its minimum reservation; acceptance transfers it without adding credit. Higher-age promotion, dominated-tail deletion and unused budgets discard credit. A macro removes at least one credit while this lane’s combined debt is positive: unfinished filtering has its own step; once filtering is empty, the lowest pending relevant minimum work is at the worker head. Credit is an analysis quantity, not machine arithmetic.

Choose fixed rates $q=64K$ macros per ordinary intermediate-name bit and $Q=1024K$ macros per target-query bit. The distinct-name busy-period argument from theorem 62 gives

$$W_{j,k}\le D_{j,k}+\sum_{d\ge1}2^d(D_{j,k}-qd)_+ \le D_{j,k}+4q\,2^{D_{j,k}/q}.$$

For lane $j>0$ let $b_j$ be its final minimum, if nonempty, and choose only for analysis

$$k=\max(4,\ell(L_j),\ell(b_j)),$$

omitting $\ell(b_j)$ if empty. Since $j<K$ and $k\ge4$, $D_{j,k}\le4Kk$, hence

$$W_{j,k}\le4Kk+256K\,2^{k/16}<1024K\,2^{k-4}.$$

The elementary last inequality is the one in theorem 62 multiplied by $K$. Lane zero uses the same inherited minimum bound with no classification. The distinct-name bound applies to each source’s actual released-name subsequence, not to free service from other sources. A fixed number of parallel copies changes the fixed machine constants only.

After this debt drains, filtering is empty and the worker is fully idle: if it received any row, a shortest numeral has completed and discarded every longer-age tail. Quiescence is locally detected by the queue/active flags and the worker head. The machine never selects the analysis cutoff or scans a queue at a delimiter.

5. Exact readout before every possible final symbol

Run all $m$ exported upper rulers from the first query bit. They cost a fixed number of pointer steps per bit and identify the unique range $(L_j,L_{j+1}]$, with $L_0=0$; beyond $L_m$ membership is false. There is no endpoint comparison at query termination.

Lane zero’s lower reader follows theorem 61. When a positive lane becomes quiescent, an empty worker permanently certifies no selected row in that lane. Otherwise capture its minimum lower ruler and use the current query-prefix unit stack as replay debt. Run four repair steps per query bit, including the birth batch. After alignment advance the lower ruler once per bit. A fixed number of lanes means all repairs run in parallel.

Put $M_j=\max(L_j,b_j)$ for a nonempty positive lane. Quiescence occurs by query time $t\le2^{k-4}$. If $k>4$, $M_j\ge2^{k-1}$ and alignment finishes by $t+\lceil t/3\rceil<M_j$. If $k=4$, the first query batch finishes the worker and its one-symbol replay. Before alignment use false for that lane. This is exact whenever its range can matter: if $b_j>L_j$, membership is false before $b_j$; if $b_j\le L_j$, repair finishes before leaving $L_j$. If $b_j>L_{j+1}$ the entire range is false, which causes no difficulty. Empty lanes can always use false.

Consequently, for every target prefix length $n\ge1$ the maintained answer is exactly

$$\bigvee_{j=0}^{m-1} \left(L_j<n\le L_{j+1}\ \wedge\ b_j\text{ exists}\ \wedge\ b_j\le n\right).$$

Indeed rows above $L_j$ all have maxima at least $L_{j+1}$, and all other rows have maxima at most $L_j$. Within this range the union therefore depends only on the least eligible lower endpoint. The empty query has false membership because all lower endpoints are positive. Complement membership for pinned Horn SAT at the prescribed final delimiter. No EOF work, padding, supplied query length or withheld final answer is used.

6. Resource and assurance boundary

Initialization has empty structures and finite flags. A producer bit uses a fixed number of current histogram/cursor observations, unary cells and strict deque operations; its delimiter performs a bounded splice. The right gate exports at most $K$ already prepared endpoints. An original left release uses $O(K)$ records and queues, a service macro uses $O(K)$ local operations, and its fixed repetition rates depend only on $K$. All old-storage observations, literal validation, names, pointer routing, preparation, allocation, suspension, delayed work, query forks, repair and output are charged to actual encoded length $N$.

Strict deque operations and inherited worker operations have finite local record plans. Unroll the fixed batches and compile the simultaneously created bounded records using the inherited compiler. This fixes degree, radius, labels, control, initialization and old-top update semantics for one automaton per fixed $K$, independent of the input endpoints and population. Logical storage is $O_K(N)$, with the inherited $N+1$ physical-node convention and $O_K(N\log(N+2))$ explicit pointer bits. New objects refer only to old roots or bounded same-batch fields compiled into the new record. No identity/address order, timing, metadata or control-flow channel supplies a maximum class.

The finite audit separately compares the gap cursor to a histogram-set oracle and the classifier/minimum receipt to a literal interval-union oracle, including retained forks and distant successors. Its tuple implementation of deque/FIFO operations is a semantic stand-in for the imported strict persistent primitives; Python timings do not establish native locality. Linked gaps and digits expose cursor operations. The all-length cost and deadline proof is written above.

Imported theorem: strict persistent catenable sequence operations. Written new argument: input-paid occupied-depth splicing and fixed-diversity threshold readout. Finite experiment: bounded semantics, forks and envelope inequalities. Conditional transfer: only the named inherited native compiler/components are used with the stated operation contracts. No new root admission, lower bound or novelty claim follows.

7. Failures, controls and next decisive test

The old fixed-cache route loses a successor beyond the changing word. Rescanning the histogram tail at a delimiter misses strict deadlines. A plain linked prefix requires unbounded reassembly; strict catenation replaces that operation. A single late pipeline bound based on the largest maximum does not protect small earlier ranges; separate boundary-scaled lanes do. Uncharged downstream release is avoided by reserving the filter and minimum budget at original release. None of these restricted failures implies nonrecognition for other representations.

The replay control is branch-local: each query fork spends its own macros and repair steps. Affine-fragment joins do not authorize independently supplied roots. Causal sharing preserves histories but does not pay observations. Unary coherent cubical machinery does not supply unbounded ordered search. Literal right-first Horn input, checked row shape, ordinary late pins and final complement output retain the native SAT controls. Entry 129’s growing alphabet, semantic quotient and matching/positive-path interface bounds are unchanged.

Next test: remove the fixed maximum-diversity gate while retaining interval rows. The present scheme allocates a lane per ordered boundary and therefore does not compile to one fixed automaton for growing diversity. Seek a sparse coverage frontier whose updates, pending comparisons and negative query certificates remain locally accessible; first test interleaved disjoint intervals and a late short interval while large endpoint work is pending. Independent-store composition remains separate.

Custody: maintained proof and checker in GitLab; primary sources remain outside public source. Claim ownership: written theorem 63 in this note, root ledger unchanged. Evidence: general proof and finite audit with explicit primitive scope. Failure/reopen contract: this section. Frontier: growing diversity and independent joins. Reader synthesis and Site: generated styled proof and highlighted, line-anchored exact-download code, with publication state recorded separately.