Independent composition: a classical lower bound with explicit costs

Working note, 1 October 2026. This audit concerns the deterministic Join-then-Query claim in SAT boundary dynamics, section 3.1. It supplies the access contract, an explicit hard-input size, a matching representation, and the limits of machine transfer.

For example, the fragments x and not-x are each satisfiable, but their Join is not. Separate preparation therefore has to retain more than one SAT bit. This note asks how much of that retained information a later combination must inspect in the worst case, even when preparation was unrestricted.

The conclusion is a sharp order-of-growth bound for this interface, obtained by applying classical set disjointness. It is not a new SAT complexity lower bound. The boundary-equivalence lemma remains a semantic foundation; none of the resource arguments below is included in its Lean verification.

1. Question and resource contract

Fix an exposed boundary B of b Boolean variables and put m=2^b. A fragment F(B,Y) denotes R_F={a: there exists y with F(a,y)=1}. Private variables of two operands are renamed apart, so their Join has relation R_F intersect R_G. The required answer is whether this intersection is nonempty.

The following contract specifies a class of implementations, not a particular layout. A program and its public parameters can depend on b but not on the two private inputs. The bound holds for every implementation in this class.

1. Each operand is separately preprocessed into a finite immutable labelled heap with a fixed finite number of opaque roots. Preprocessing can use arbitrary time and finite space. The two heaps are disjoint except for fixed, input-independent, pointer-closed data. No joint preprocessing, shared mutable cache, input-dependent global state or operand-specific executable code is available without being represented and charged.
2. Left and right handles have at most h_L and h_R scalar metadata values. Root presence, tags or lengths that are supplied as ordinary scalars must be included here. The number and order of roots are fixed. Raw root addresses carry no observable information.
3. Pointer ports have fixed names. Following or copying an opaque old pointer produces another opaque pointer. It cannot branch on that pointer’s numeric value, physical identity, existence or heap ownership. Missing ports are totalized to an absorbing missing endpoint. Testing missing, reading a label or otherwise obtaining information about old storage is a probe. Each probe reads only the endpoint of one selected old reference; its answer is determined by that operand’s heap and the public probe instruction. There is no primitive jointly inspecting the two private heaps. Every probe has at most g possible observable outcomes, where g>=2.
4. All control choices, fresh labels, pointer selections, timing visible to the program and halting decisions are deterministic functions of public parameters, handle metadata and previous probe outcomes. Fresh records may contain copied opaque pointers. Reading their already known fields discloses no new input information. Allocator addresses, pointer comparison, exceptions, memory exhaustion and timing cannot supply uncharged channels.
5. The algorithm terminates with the exact Boolean answer on every valid pair. T is its worst-case number of old-information probes from receipt of both handles through the answer. Deferred Query work counts. Navigation, fresh allocation and computation are free for this lower-bound measure, which only strengthens the permitted algorithm. Their actual costs must be counted separately in any implementation upper bound.

This contract is checkable at the instruction level: identify every operation that can affect control or expose a value, classify its provenance and outcome alphabet, and check initialization. It does not assume the desired lower bound. In particular, a syntactically finite instruction is not automatically a constant-information probe if its return value is an unbounded word.

2. Proposition and proof

Proposition (classical disjointness application). If the interface accepts all finite 3CNF fragments over B, where clauses may have size at most three, then

$$h_Lh_R g^T\ \ge\ 2^{2^b}, \qquad \log_2 h_L+\log_2 h_R+T\log_2 g\ \ge\ 2^b. \tag{A}$$

The same bound applies to an interface returning a reusable Join handle when an exact Query is included in T. It is already necessary for the weaker task of returning only one Boolean answer. For fixed metadata and outcome alphabets, T=Omega(2^b). No representation-size limit is required for this lower bound.

Simulation. Alice receives a subset X of U={0,1}^b and Bob a subset Y. Section 3 constructs fixed-shape 3CNFs with relations X and Y. Each party runs its separate preprocessor. Reveal the two handle metadata values, partitioning the input pairs into at most h_L h_R classes.

Represent every old reference in the public simulation by an owner, a root index and a finite port word. These are symbolic expressions, not physical addresses. Two expressions may name the same node without the simulation knowing that fact. Missing endpoints stay symbolic until probed. A path remains assigned to its original owner even if it reaches fixed common initialization; that owner can compute the answer. Identity is unobservable, so duplicating that fixed initialization does not change the program’s behavior.

Between probes, both parties perform the same symbolic computation. Fresh records have public identifiers and known fields containing public values or symbolic references. Following a fresh field yields its known symbolic value; following an old field appends a port name. At a probe the owner of the selected old expression returns one of g outcomes. Thus the next expression, its owner, all control and the stopping decision are determined by the shared history. This invariant proves the simulation by induction on instructions. Arbitrarily long silent computations cause no problem: they are the same on every input pair with that history, and termination is assumed. No input-dependent silent stop signal is available.

Each terminal history describes a rectangle A times D of inputs. Initially the metadata restriction is a product restriction. At a probe only the owner’s possible inputs are restricted by its response, preserving rectangularity. At a terminal history the answer is public and hence constant on the rectangle.

There are 2^m disjoint pairs (X,U minus X). Two distinct such pairs cannot belong to the same rejecting rectangle: at least one of X minus Z and Z minus X is nonempty, so one crossed pair has nonempty intersection. Therefore at least 2^m rejecting leaves are needed. After the metadata prefix, a tree of at most T g-valued probes has at most g^T leaves. Multiplying by the metadata choices proves (A). This also avoids rounding to binary message lengths; the previous inequality with ceilings follows immediately.

The proof is the standard deterministic rectangle/fooling-set argument. The work specific to this note is making the storage-to-protocol simulation and its qualifications explicit, not discovering a new communication theorem.

3. Hard fragments and actual formula size

The older construction forbids each excluded boundary assignment and splits each resulting long clause. It can use O(bm) literal occurrences. A complete binary decision tree gives a more economical, fixed-shape family.

For every binary word p of length at most b introduce a private variable z_p. For each internal node p of length d<b, impose

$$z_p=\begin{cases}z_{p0}&x_{d+1}=0,\\z_{p1}&x_{d+1}=1.\end{cases}$$

Encode this with the four clauses

$$\begin{split} &(x_{d+1}\vee\neg z_p\vee z_{p0}),\quad (x_{d+1}\vee z_p\vee\neg z_{p0}),\\ &(\neg x_{d+1}\vee\neg z_p\vee z_{p1}),\quad (\neg x_{d+1}\vee z_p\vee\neg z_{p1}). \end{split}$$

For each leaf a, pin z_a to 1 exactly when a belongs to X. Finally require z_empty=1. For a fixed boundary assignment, the leaf values determine all internal values uniquely, from the bottom up. The root is precisely the leaf selected by that assignment. Thus existential projection is exactly X. This proves the representation for every b, including b=0, when the two root unit clauses either agree or contradict.

There are m leaves and m-1 internal nodes. For one fragment the exact counts are

$$V=b+2m-1,\qquad C=5m-3,\qquad L=13m-11, \tag{B}$$

where V counts all variables, C clauses and L literal occurrences. The formula shape, variable names and clause lengths are independent of X; only leaf-unit signs change. Separate operands use distinct private namespaces. Hence the entire fooling family has the same description size at each b.

To specify bit size, number variables 1 through V. Encode each clause length in two bits and each literal by one sign bit plus k=ceil(log_2(V+1)) identifier bits. A self-delimiting header for b,V,C uses O(b+1) bits. For b>=1, k=b+2, so each explicit fragment uses

$$N_b=2(5m-3)+(b+3)(13m-11)+O(b) =\Theta(b2^b). \tag{C}$$

Let N be the combined explicit bit size of the pair. On this hard family, N=Theta(b2^b), log N=Theta(b), and fixed-alphabet (A) gives

$$T=\Omega(N/\log N).$$

In literal occurrences it is a linear lower bound, Omega(L). If the input is instead the fixed-tree template plus its m leaf bits, its description size is Theta(m), and the bound is linear in that encoding. These are different input representations. None of them establishes a superpolynomial lower bound in actual input size. Nor does this family establish exponential cost for every formula of size polynomial in b.

The construction uses ordinary Shannon expansion and gate-definition CNF. It improves the explicit size accounting of the earlier witness; it is not a new succinctness theorem.

4. A matching persistent upper bound

Separately preprocess each arbitrary finite fragment into its m-bit boundary truth table, in a common lexicographic order. Exhaustive assignment evaluation is one terminating preprocessor. Its time may be enormous and is not part of the post-preprocessing bound. Store the table as an immutable singly linked list with labels Zero, One and End; retain the syntax under a separate opaque root if the interface must preserve it.

For the Boolean answer, scan the lists together and test their two bits at each position. There are at most 2m+2 old-label probes and O(m) ordinary pointer steps. Only a fixed number of cursors and finite control bits are needed.

For a reusable Join result, scan all positions, cons each bitwise conjunction onto an accumulator, and reverse that accumulator in a second pass. This uses O(m) local steps and at most 2m+O(1) fresh records; every microstep has constant radius and allocation. Cache whether any output bit is One. The result’s Query is then constant time. Attach a constant-size syntax Join record referencing the two original syntax roots; its decoder uses independent private renaming at each occurrence. All old tables, syntax and handles remain unchanged.

The reversed intermediate list is necessary: silently appending to an immutable singly linked list would not have constant local cost. Work inspecting the intermediate list is O(m) too, whether classified as fresh information in the whole operation or as old storage relative to the next microstep.

Consequently the optimal worst-case post-preprocessing probe growth in this constant-information interface is Theta(2^b), up to constant factors, using a fixed alphabet large enough for the listed tags. This is not optimality for every metadata/word-size tradeoff, preprocessing time, storage succinctness, one-step allocation or other SAT operations.

5. What reaches machine mechanics

If each machine transition can acquire at most P of the counted old outcomes, then T<=Pt. Equation (A) directly gives

$$\log_2 h_L+\log_2 h_R+Pt\log_2 g\ge 2^b. \tag{D}$$

This conclusion requires the same independent initialization and absence of other information channels. It is a direct simulation argument, not a converse of a compiler theorem.

For a bounded-view record machine with s roots, arity q and endpoint radius r, one sufficient bound is P=s sum_{j=0}^r q^j. A native scaffold view likewise has a finite bounded number of port positions at fixed degree and distance. Thus an independently supplied two-fragment interface obeying this contract cannot finish in a constant number of such transitions uniformly in b when all its finite alphabets and metadata bounds are fixed. This statement does not cover a sequential recognizer that performed joint work while reading the inputs.

A separate direct TM case is also precise. Give a deterministic machine a fixed number K of separately preprocessed work tapes, each tape belonging to one operand, and a fixed tape alphabet Gamma of size at least two. Initial controller information about the inputs is confined to the handle metadata; initial head locations serve as separate relative origins. At most K original tape symbols are read in a transition. Head moves and writes are determined by the public history; overwritten cells then contain publicly known symbols. Simulating the original-symbol reads therefore proves (D) with P=K and g=|Gamma|. This is an independently preprocessed tape phase, not the ordinary all-blank input-machine convention and not a lower bound for arbitrary TMs deciding raw SAT.

The reviewed record compiler can translate a fully specified finite-rule loader and the list-scan microsteps into a scaffold, with one transition per explicit input/clock step, degree max(1,s+Aq), and native distance r+1. Its fixed pointer-closed initialization premise still has to hold. It does not turn an input-dependent preloaded heap into free initialization or compress O(m) scan steps into one Join letter. The existing strict multitape transfer likewise assumes an all-blank initial tape. No new source-to-scaffold or TM application was kernel checked here. A subsequent scaffold-to-PEG transfer would reverse the actual encoded input language.

6. Sources, status and conclusion

Sherstov’s Thirty-Five Years of Set Disjointness, section 2, records the rectangle method and the complement-pair fooling set used here. We reproduce the argument rather than claim a new communication lower bound.

Miltersen, Nisan, Safra and Wigderson, On Data Structures and Asymmetric Communication Complexity, sections 1.1 and 2, Lemma 1, explicitly translate cell probes into communication, charging an address message and a cell-content reply. Their addressable-cell model is not silently identified with ours: here the opaque root/path expression is already determined by the transcript, while every observable old value is charged. Their stronger data-structure bounds are not imported.

Bryant’s Graph-Based Algorithms for Boolean Function Manipulation develops the Shannon-expansion decision-graph framework. The full-tree witness above uses that elementary expansion without relying on a new decision-diagram algorithm. The four defining clauses and their projection property are proved directly in this note.

Status. Written unbounded proofs with separately scoped finite checks; not a new Lean proof or external peer review. The quantitative mechanism is classical set disjointness. The exact pointer contract, explicit input accounting and matching persistent scan make this a useful worked application. They do not establish an additional fundamental lower-bound principle.

The unrestricted-relation, constant-information composition question is settled to order Theta(2^b) after arbitrary independent preprocessing. We close this claim as a classical application. A lower bound for compact fragments or for polynomial-space preprocessing would require a new, expressly specified hard family and resource argument; it does not follow from this audit. General bounded persistent realization remains unresolved.

The finite checker and recorded scope exercise the gate truth table, small complete projections, complement fooling pairs, explicit size counts, and immutable table scans. They do not verify arbitrary programs, all heaps, the universal lower bound or a compiler implementation.