Sealed affine boundaries: small summaries and the cost of maintaining them
Our goal is to understand representations maintained by finite rules with bounded local access and allocation. For independently prepared affine fragments, a useful distinction is between a summary that remains small and the work required to produce that summary after a join. Classical elimination supplies the first; it does not make the second free.
Contents
What future operations may see
Fix an ordered boundary , with . A fragment is a system
where is private. Different operands’ private variables are renamed apart. Future operations may conjoin affine constraints on and ask about the resulting boundary relation, including membership and satisfiability. They cannot expose , identify private variables across fragments, inspect internal witnesses or count private extensions. Call this a sealed boundary. The common ordering is part of the input convention, not a free name-matching algorithm.
For example, and have the same unconstrained projection onto an unrelated boundary. If a future operation can inspect , that projection is no longer a sufficient summary. Likewise, a free private bit and a pinned private bit have identical boundary relations but different numbers of extensions. Sealing is an actual restriction on future observations.
The classical summary
The projected relation is empty or has a description
with at most independent equations. It needs coefficient bits, plus a distinguished false flag. Eliminating private columns in yields a block of equations with full-row-rank private coefficient matrix and a remaining block . For any satisfying the latter block, the private equations have a solution. Reducing the remaining block gives the summary, or detects inconsistency.
This is classical affine projection, not a new semantic lemma. For an explicit published statement, see Bruno Zanuttini, Research Note: New Polynomial Classes for Logic-Based Abduction, Lemma 1 (2003). The additional bound of nonredundant equations is ordinary rank reduction.
For independently prepared fragments with disjoint private variables,
Stack their summary equations and reduce again. The output still has at most equations. Inductively, this bound is independent of the number, interior size and arrangement of previous joins. This uses the existing boundary semantics; it does not establish a new general characterization of persistent computation.
Explicit local cost, with persistence
A uniform implementation can store each bit in a finite-tag immutable list node and each equation in a row list. The boundary has a unary ruler. No numeric pointer, identity comparison, random array access or input-sized control table is required.
At a join, there are at most rows of length . Keep a full row and a cursor at its current column in a bounded-arity row descriptor. For each of the columns:
- Scan the row descriptors to find a nonzero pivot among the unprocessed rows, if any.
- Sweep those rows, XORing the full pivot row into rows whose current bit is one. A synchronized list scan and reversal creates each new row in primitives and nodes. An immutable prefix ruler locates its current-column cursor in another scan.
- Advance all remaining column cursors once and retain the pivot as a completed equation.
Earlier pivot positions in the unprocessed rows are zero, so these operations implement ordinary forward elimination. At most stages each touch rows with work per row. A final scan detects a zero coefficient row with right-hand side one. Otherwise copy the retained equations into a clean output list, omitting descriptors and temporary roots. That last copy ensures the summary’s reachable graph has nodes and does not accidentally retain the old operand chain.
Thus an eager join has the written bounds
Each primitive performs bounded local access and allocation. The whole join is not a constant number of primitives uniformly in . Old operands remain valid. A cached consistency flag answers satisfiability in constant time after the join has completed. Membership in a supplied assignment takes local steps, including repeated sequential assignment scans.
All temporary and abandoned nodes remain charged. For actual joins, including alternative retained or discarded versions, total historical allocation is
where bounds the preparation and allocated history of leaf . Small reachable summaries do not imply small total history or free garbage collection. For , a single consistency bit suffices; replacing by covers that case uniformly.
For a leaf with equations over total variables, a deliberately coarse list-elimination budget is time and nodes, including a final summary copy. Dense input with unary dimension headers has bits, so this is polynomial in actual input size. This is a native linear-equation input convention, not a claim of bounded-time parsing or solving arbitrary CNF. Explicit node references throughout a history of nodes cost bits; node counts must not be confused with the earlier small linear-bit storage budget.
Why small summaries do not imply cheap joins
The overlapping affine compatibility result fits this sealed interface with :
It already gives worst-case old-information observations for join plus final consistency answer, under the independent address-blind finite-outcome contract, even allowing arbitrary separate preparation. In particular, no alternative summary implementation makes both operations uniformly constant for growing in that model.
Conversely, summaries can be read completely in old-information probes and reduced using computation on the observed data. Thus worst-case probe order for this class is when computation and fresh allocation are free. The explicit local implementation above supplies time, not a matching quadratic time result. This gap is not selected as a new optimization target.
The hard subfamily has dense size and named fixed-shape CNF size , as accounted for in the linked proof. Arbitrarily large private interiors affect preparation; after projection, they do not increase these join bounds.
What this resolves, and what it does not
A sealed interface and closure of its summaries under conjunction give a representation whose active description does not grow with composition depth. Maintaining that description still requires paid normalization. A constant-time lazy pair can defer this normalization, but then the consistency query pays for it. The cheap row-functional queries in the earlier readiness construction have a different contract and remain valid.
This is explanatory synthesis of classical elimination and the preceding reviewed lower bound. The local resource argument is written and independently reviewed, not formally verified. No new finite experiment, novel classification or constant-cost growing-boundary construction is claimed. Fixed gives only a finite-state special case already covered by the existing finite-quotient result.
The remaining structural question concerns when growing interfaces support a useful bound on deferred work with only bounded work at each external operation. Small semantic summaries alone do not answer it. A further candidate must specify its future observations, normalization obligation and resource tradeoff before it merits another theorem campaign.