SAT fragments: future behavior, information and persistent dynamics

Working research note, 1 October 2026.

Overview

A fragment that is satisfiable today may conflict with a fragment added tomorrow. The one-clause fragments x and not x, for example, are each satisfiable but incompatible. A reusable representation must therefore retain more than the current yes-or-no answer: it must retain exactly which assignments to its exposed variables can still be extended to a solution.

That set of extendable assignments is the fragment’s boundary relation. This note proves that the relation completely determines every future observation allowed here, then asks how much information and local access are needed to maintain it. The answer depends sharply on the constraint language: 2CNF and affine fragments have quadratic-size boundary summaries, while general 3CNF and Horn fragments can have exponentially many boundary bits. For any fixed boundary width, finite persistent implementations still exist, and the note gives both an immutable construction and an explicitly clocked Turing-machine route.

These are interface and machine-model results, not lower bounds for arbitrary SAT algorithms. The main unresolved case is growing-width Horn composition: two fragments can exchange a short compatibility transcript, but computing each local closure from immutable data may still be expensive.

1. Values, interfaces and observations

A b-boundary fragment is a Boolean formula F(B,Y), where B=(x_1,…,x_b) is an ordered list of distinct exposed variables and Y is a finite set of private variables disjoint from B. Its private variables are existentially bound. Values retain the actual formula modulo renaming of private variables; they are not identified merely because they have the same satisfying assignments. A 3CNF here has clauses of size at most three; unit and empty clauses are allowed. Empty conjunction is true and empty clause is false.

Define its boundary relation

$$R_F=\{a\in\{0,1\}^b:\exists y\ F(a,y)=1\}.$$

Join identifies corresponding boundary variables and first renames the private variables of its operands apart. Thus even Join(h,h), using the same retained handle twice, has two independent sets of private variables. Physical pointer sharing is not semantic identification of bound variables. Query asks whether the current fragment has a satisfying assignment, i.e. whether R_F is nonempty. Future contexts may conjoin further fragments, introduce fresh exposed variables, forget exposed variables, and permute boundary positions. They may never refer to a variable once it has become private. Every boundary assignment can be pinned by a conjunction of positive or negative unit clauses. This last assumption is essential and is explicit in every equivalence below.

Lemma 1 (boundary equivalence). Two fragments of the same boundary sort have identical satisfiability observations in all these future contexts if and only if their relations R_F are equal. Already the contexts consisting of one Join with a pinning fragment, followed by Query, suffice for necessity.

Proof. With private variables renamed apart,

$$R_{F\mathbin{\Join}G}=R_F\cap R_G.$$

For each fixed boundary assignment, satisfying witnesses for the disjoint private sets can be chosen independently, proving both inclusions. Introduce adds a free coordinate, forgetting projects existentially, and permutation permutes coordinates. Each is a function of the relation alone, so induction on a future context proves sufficiency. For necessity, if a belongs to exactly one of R_F,R_G, join the unit conjunction P_a that fixes B to a. Exactly one of Join(F,P_a), Join(G,P_a) is satisfiable. This proves the claim.

This is the familiar existential-projection semantics of constraints and logical forgetting, now used as a syntactic quotient. A useful negative control is to allow only nonempty positive clauses and positive contexts: every such formula is satisfiable by the all-one assignment, so distinct relations may be observationally equivalent. Pins of both signs cannot silently be omitted. A second negative control is accidental private-variable sharing: the closed fragments y and not-y each have relation {()}, but conjoining them without renaming is false. Lemma 1 would fail for that different operation.

Lemma 1 now has a Lean-checked formalization for concrete Boolean syntax, typed repeated-input contexts and finite adaptive SAT clients. The later counting, resource and machine-construction results below are outside that formalization and retain their separately stated proof status.

2. How many future types are there?

Let N_C(b) be the number of distinct boundary relations realized by a constraint class C, allowing arbitrarily many existential private variables. The contexts include unit pins within that class. Put H_C(b)=ceil(log_2 N_C(b)). This is the minimum number of bits in a fixed-length exact semantic summary code; it is not a measure of solver running time or of the entire stored formula.

Theorem 2 (contrasting information growth). As b grows:

The asymptotic claims concern b>=2. All four classes have a finite quotient for each fixed b. The differences concern growth with b. In particular, tractable Horn satisfiability can coexist with exponentially large boundary information. These are worst-case counts over all finite fragments; they do not assert exponential compilation from every small input or every individual Horn formula.

2.1 Every Boolean relation has a 3CNF presentation

Given R subset {0,1}^b, for each a outside R make the clause D_a that is false exactly at a: use x_i when a_i=0 and not-x_i when a_i=1. The conjunction of these clauses has satisfying assignments exactly R. For b=0 use true or the empty clause. Convert a clause l_1 or … or l_m with m>3 to

$$(l_1\vee l_2\vee z_1)\land \bigwedge_{j=2}^{m-3}(\neg z_{j-1}\vee l_{j+1}\vee z_j) \land(\neg z_{m-3}\vee l_{m-1}\vee l_m),$$

where all z variables are fresh for that clause; the middle conjunction is empty when m=4. Existential projection of this gadget is the original clause. If all literals are false it forces every z true and then contradicts the last clause. If some literal is true, take z_j true exactly when the first j+1 literals are all false. Every gadget clause is then satisfied. Independent fresh variables let the gadgets be conjoined without changing the projection. Hence every R is realizable. There are exactly 2⁽²b) possible relations.

This is the standard clause-splitting reduction with its stronger projection property spelled out. It also admits a supplied slot construction using at most b+2 simultaneously exposed variables: retain the b boundary variables and at most two adjacent gadget variables, forgetting a gadget variable after its final occurrence. This is a sufficient width bound, not an optimum.

2.2 Binary clauses: a quadratic summary

Eliminate a private variable y from a 2CNF by resolving each clause y or a with each clause not-y or c, adding a or c, and removing all y-clauses. Here a or c can be absent for a unit clause. For any assignment to the other variables, failure to extend to either y-value occurs exactly when some such opposing pair forces both values. Thus the resolvent formula is precisely existential elimination. Clauses remain of size at most two. Iteration proves that R_F has a 2CNF presentation on B alone.

There are at most 1+2b+4*binom(b,2) non-tautological clauses of size at most two, including empty and unit clauses. Their presence bits give H_2CNF(b)=O(b^2). A canonical choice is the set of all entailed clauses of these sizes.

For the lower bound partition B into U,V with sizes floor(b/2),ceil(b/2). For each E subset U x V take the implications u->v indexed by E. To test edge (u,v), set that u true, all other U variables false, that v false and every other V variable true. This assignment fails exactly when (u,v) is in E. Consequently the 2^(|U||V|) edge sets give different relations, and H_2CNF(b)>=floor(b^2/4).

2.3 Affine constraints: another quadratic summary

Conjunction of affine equations intersects affine solution sets; projection under forgetting is a linear map of an affine set, hence affine or empty. Gaussian elimination gives a presentation of any nonempty relation by at most b independent equations on b variables, with right-hand sides. A matrix and an empty-relation marker require O(b^2) bits.

For the lower bound use the same partition and all binary matrices M of size |V| by |U|. The graphs v=M u are distinct linear subspaces, distinguished by a unit vector u wherever two matrices differ. There are 2^(|U||V|) such graphs. If desired, long XOR equations can be split with private partial-sum variables into constraints of arity at most three. XOR constraints are a different allowed relation language, not ordinary disjunctive 3CNF clauses.

2.4 Horn constraints: exponential information despite tractable SAT

Identify an assignment with its set of true coordinates. Let t=floor(b/2), b>=2. For any family X of t-element subsets of B, put

$$\mathcal H_X=\{S\subseteq B:|S|<t\}\cup X.$$

This family is closed under intersection. More explicitly it is defined by negative clauses forbidding each t-set outside X and every (t+1)-set. Thus sets below size t are admitted, precisely X is admitted at size t, and all larger sets are excluded. Different X give different relations. There are 2^binom(b,t) choices of X.

Every negative clause is Horn. The clause-splitting gadget above preserves Horn form when the original clause is all-negative: an intermediate clause has only the new z as a positive literal; the final clause is all-negative. Thus fresh existential auxiliaries give Horn 3CNF presentations of all these relations. More generally, a long Horn clause can be split by placing its possible positive literal last. This proves the lower bound using literal Horn formulas, without relying on a characterization theorem for closure systems. The universal truth-table bound gives H<=2^b.

The construction counts many relations, including formulas that have long presentations. It does not prove that every Horn representation is large, or that auxiliary-variable circuits cannot compactly represent particular relations. Linear-time static Horn SAT and this information bound concern different requirements.

3. From semantic information to an old-view resource bound

Use the standalone immutable record model of the operational syntactic-algebra theorem: finite labels and handle metadata; fixed root count and pointer arity; immutable old records; fixed finite pointer-closed initialization; independent copies can be combined; no identity tests, address arithmetic, hidden global history or uncharged scan. Both observations and copied old addresses count against the radius. Finite rules choose from endpoint-labelled unfoldings, not physical sharing patterns. No external boundary-assignment oracle is available.

For a particular b, suppose every fragment in the chosen class has a valid handle; Join works on any valid pair with matching b-boundary, and Query is immediate and exact. Let s be the number of roots per fragment, h the number of possible handle-metadata values, and g the number of endpoint observations, including all fixed special labels and missing. Let q>=1 bound pointer arity. Let r_J,r_Q bound Join and Query in the endpoint convention, and set R=r_J+r_Q. All constants may depend on the implementation or on b; the inequality makes that dependence visible.

Theorem 3 (local-view information bound). Necessarily

$$\boxed{\quad \log_2 N_C(b)\le \log_2 h+s\!\left(\sum_{j=0}^{R}q^j\right)\log_2 g. \quad} \tag{1}$$

Proof. Fix one valid handle for a representative of each relation. A radius-R view is determined by its metadata and the endpoint labels for at most ssum(q^j) root/port positions. There are at most hg^(s*sum(q^j)) views. Equal views of F and G give equal answers after Join with any independently constructed pinning fragment and then Query. The composition radius is R: a query path through fresh records exits to an old target within r_J of an input root and adds at most r_Q further edges. Fresh labels are determined by the same old views. Lemma 1 therefore forces R_F=R_G. The view count is at least N_C(b). Taking logarithms proves (1); for the integer summary length the consequence is H_C(b)<=ceil(RHS). No information bound is obtained from allocation alone. Large fresh batches chosen from the same finite view cannot distinguish its members.

For fixed h,s,g and q>=2 this yields:

• all 3CNF fragments: R >= b/log_2 q - O(1);
• Horn 3CNF fragments: R >= (b-O(log b))/log_2 q;
• 2CNF and affine fragments: R >= 2 log_q b - O(1).

For q=1, the corresponding lower bounds on R+1 are respectively Omega(2^b), Omega(binom(b,floor(b/2))), and Omega(b^2). These concern uniform Join followed by immediate exact Query, with fixed metadata/label resources. They are not optima, general SAT time lower bounds, or restrictions on arbitrary offline, amortized or mutable algorithms. Increasing the label alphabet or number of roots can trade against radius, as (1) states.

In particular, no one fixed choice of all these resources works for every b, even for 2CNF. With arbitrary globally named variables the simpler unit-clause example x_i versus x_j, tested by not-x_i, already gives infinitely many types. This does not depend on P versus NP. It rules out the stated standalone join interface, including joins with arbitrary previously constructed fragments.

3.1 A stronger total-access obstruction for arbitrary 3CNF

The composition-access audit now gives the exact instruction-level contract, including silent navigation and halting, a fixed-shape hard family, actual input-size accounting, and a matching persistent scan. It closes this claim as an application of classical set disjointness. The bound is linear in that family’s literal count, not a superpolynomial raw-SAT bound.

Radius counts how far an operation reaches. We can also count how much old information it actually acquires. Consider a deterministic algorithm receiving two independently constructed fragment handles. Their private heaps are disjoint, apart from fixed initialization that can be duplicated without any observable identity test. The algorithm may navigate and copy opaque pointers, allocate fresh records, and adapt its probes. Every observation of old storage, including a missing endpoint, returns one of g>=2 outcomes. Raw addresses, pointer identity, uncharged scalar fields and hidden input-dependent state are excluded. Let T be the worst-case total number of such old-storage probes used by Join followed by exact Query. Allow arbitrary preprocessing of each operand separately; no joint preprocessing is supplied. There are h metadata choices per handle. Count every input-dependent observation, not just distinct labels.

Theorem 3a (communication-to-access bound). For all b-boundary 3CNF fragments, every such implementation satisfies

$$2\lceil\log_2 h\rceil+T\lceil\log_2 g\rceil\ \ge\ 2^b.$$

In particular, with fixed h,g it requires Omega(2^b) old-information probes in the worst case, independently of the chosen representation or allocation allowance. This is a bound for the specified independent-fragment interface, not for ordinary SAT on a raw input of size b.

Proof. Put U={0,1}^b and m=|U|=2^b. By Section 2.1 each subset X of U has a 3CNF representative. Alice receives X and constructs its chosen handle; Bob does the same for Y. They first exchange handle metadata. They then simulate the algorithm publicly. Each opaque old reference can be named in the public simulation by its owner, input root and port path; this symbolic name is not an address observed by the algorithm. Navigating or copying it requires no communication. At an old-information probe, its owner sends the one g-valued observation. Fresh records and control are determined by the public transcript. Shared initialization may be unfolded separately on each side because identity is unobservable. Thus the simulation communicates at most the left-hand side of the inequality and decides whether X intersects Y.

Here is the full classical lower-bound argument. A transcript of a deterministic two-party protocol determines a rectangle of input pairs: each message restricts only its sender’s possible input. All pairs in a terminal rectangle have the same answer. The 2^m pairs (X,U minus X) all have empty intersection. For two distinct sets X,Z, at least one crossed pair (X,U minus Z) or (Z,U minus X) has nonempty intersection. No rejecting rectangle can therefore contain two of these pairs. There must be at least 2^m terminal transcripts, and a binary protocol of worst-case cost C has at most 2^C leaves. Hence C>=m. This is the standard set-disjointness fooling-set proof, not a new communication lower bound.

The hypotheses are essential. A unit-cost lookup returning an unbounded summary violates the g-valued observation limit. Address arithmetic or identity may disclose information omitted by this simulation. A representation jointly preprocessed for this particular pair is a different interface. No randomized or amortized extension is asserted here. The hard fragments may themselves have large formulas, so this result says nothing about P=NP.

3.2 Horn composition shows why summary size is not interaction cost

In the two-party communication model, each party may perform unlimited local computation on its own fragment. Only transmitted bits are charged. Even though Horn boundary summaries have exponential information, their joint satisfiability has a short interactive protocol.

Theorem 3b (Horn closure protocol). Two arbitrary Horn fragments sharing b boundary variables can decide satisfiability of their correctly renamed join using O(b log(b+1)+1) communicated bits. This includes existential private variables and allows each fragment to be unsatisfiable.

Proof. Horn satisfying assignments are closed under coordinatewise meet: if a Horn implication’s antecedent is true in a meet, it is true in both operands, and its conclusion is true in both. A negative clause cannot become false under a meet unless it was already false in both. Existential projection preserves meet closure by taking the meet of witnesses. Thus each boundary relation R is a finite meet-closed family of subsets of B, possibly empty.

For S subset B, let c_R(S) be the intersection of all members of R containing S, or report failure when none exists. In the nonfailure case c_R(S) itself belongs to R and contains S. It is the least model extending S. Start from S=empty and alternate c_R_F and c_R_G. A party reports failure, reports the newly forced boundary coordinates, or reports no change. On failure reject; after two successive no-change reports accept.

Every common model contains S throughout: a closure replaces S by the least model of one side extending it, still contained in that common model. Consequently failure correctly excludes every common model. Two unchanged closures give S in both relations, a witness for acceptance. Each changing turn adds at least one coordinate, so there are at most b changing turns, at most b+2 unchanged turns before termination, and at most b transmitted coordinate names in total. End-of-message and failure flags plus fixed-length coordinate codes give the stated bound. A rejected turn also halts immediately.

This is alternating least-model closure, built from the standard Horn fixed-point principle. It does not implement a closure lookup with bounded record access. A party may need to inspect its entire fragment to compute c_R(S); that local work is free only in the communication model. Accordingly the Horn information bound in Theorem 2 cannot simply be substituted into Theorem 3a to assert exponential communication. General 3CNF has Theta(2^b) deterministic communication (send one truth table for the upper bound), while Horn has the polynomial upper bound just proved. For 2CNF and affine fragments, sending their O(b^2)-bit boundary descriptions also gives polynomial communication, without any optimality claim.

These results distinguish three measurable quantities: how many future behaviors exist, how much information two independent fragments must exchange, and how much local work realizes that exchange. None can silently replace the other two.

4. A finite constructor calculus at fixed width

Fix w>=0 boundary slots [w]={1,…,w}. Sorts are the subsets S of [w]. A value has precisely the exposed slots S, with private variables bound. Use this finite signature:

A reused slot after Forget denotes a new variable, not the previously hidden one. At Join, identify only equal exposed slots and rename private interiors apart. These conventions are part of the values and operations, not a resource-intensive runtime name-resolution algorithm. Inputs are instructions using the fixed slot alphabet.

Theorem 4 (persistent finite-width realization). For every fixed w this calculus and Query have a finite-rule immutable implementation with one root per supplied value, pointer arity q<=2, endpoint radius r=0, and at most one fresh record per constructor (zero for Query). It preserves exact fragment values up to private alpha-renaming and every retained version across arbitrary valid construction histories.

Proof. Each sort S has at most 2⁽²|S|) possible relation tags. Store S, R and the constructor name at the root, along with at most two input pointers. Each relation update is a fixed finite table. The decoder recursively applies the formula constructor, with independent private renaming at each Join occurrence. Thus even a shared DAG unfolds to independent bound-variable occurrences when required. Induction on creation time proves the relation invariant, exact formula interpretation and persistence. All old pointers copied are supplied roots; all inspected data are root tags. Each Empty_S request can create its one constant record, so the initial heap may be empty and is pointer-closed. Exact printing of the unfolded formula is a separate operation and may be expensive.

This is an existence construction for each w, with enormous possible finite tables. A tag carries up to 2^w truth bits. It is not a uniform constant-bit algorithm as w grows. Formula equality and graph identity are not observations. The finite-algebra theorem also supplies stored-context transformations and uniform Apply at fixed w, if that larger interface is requested.

Relation to treewidth

A well-formed construction tree has a primal-variable tree decomposition of width at most max(w-1,0): use the live variables S at each constructor node, identifying boundary variables through edges and joins and renaming private ones as above. Each clause is covered by its Add bag. A variable’s occurrences form a connected set because a forgotten variable cannot reappear and a join identifies only exposed coordinates. For an empty variable graph the usual width -1 convention can instead be used.

Conversely, a supplied nice primal decomposition of width k can be translated into such a construction with w=k+1. Assign each clause to a bag containing its variables, use Introduce/Forget at bag changes, Join at equal-bag branching, and consistent local slot names along each edge. A clause’s variables form a clique, hence occur in a common bag: their connected bag subtrees meet pairwise, and finite subtrees of a tree have the Helly property. Unit and empty clauses are immediate. This is the standard decomposition construction; finding a decomposition, checking a supplied raw one and resolving arbitrary variable names are additional input tasks. We do not charge them zero time.

For a DAG of construction records, this statement concerns its unfolded formula with the specified private renaming. It does not claim that the physical record DAG has bounded treewidth. The unrestricted b-boundary counting theorem and the live-slot bound w are separate parameters; Section 2.1 relates them by a sufficient w=b+2 construction.

5. A concrete scaffold client

An interface accepting arbitrary supplied handles is not by itself a fixed-root scaffold controller. Here is a complete client. Read a postfix word over the finite constructor alphabet of Section 4. Constants push a value; unary constructors replace the top value; Join pops the top two values and pushes their join. Check sorts and underflow, sending invalid inputs to a permanent reject state. Accept precisely when the word has left one value of sort empty whose relation is {()}. Empty input rejects. Call this finite-alphabet language K_w. It encodes construction instructions, not a raw DIMACS formula.

Theorem 5 (postfix scaffold realization). For each fixed w, K_w has a degree-five, native-distance-three scaffold recognizing the same input words and preserving the decoded persistent evaluation described below. For language recognition and the semantic operand stack alone, degree one and native distance two suffice, and distance two is necessary.

Maintain one root to an immutable operand stack. A stack record has a value pointer and tail pointer; a value record has at most two operand pointers. The fixed initial graph contains only Bottom. A unary operation allocates a value node and a replacement stack node. A Join reads the top two nodes and value tags, allocates its value node and its new stack node. A constant request allocates both a fresh value record and a stack node; it does not reach for a remote initialization record. The stack node records whether its tail is Bottom; finite control caches the acceptance bit of the current configuration. Every pointer needed is within two old edges from the stack root, including the second value root and the tail after two pops. The copied old targets, not only the tested labels, are covered.

Thus the whole client has

$$s=1,\qquad q=2,\qquad A\le2,\qquad r\le2.$$

The reviewed simultaneous-record compiler gives an ordinary scaffold for K_w with degree max(1,s+Aq)=5 and native distance r+1=3, one append per instruction. These bounds are independent of w, but its finite labels and controller are not. No optimum is claimed. The source client preserves the exact operand fragments and all old operand-stack versions. The scaffold preserves them through the compiler’s decoder, not by identical raw graphs. Distance-two normalization is available at additional degree cost, but is unnecessary here.

An induction on the postfix word proves the stack matches the evaluation of its maximal completed term forest. Type checking and the singleton-root test prove recognition, including malformed words and epsilon. Consequently this is an actual application of the compiler beyond palindrome construction.

A smaller recognizer and a sharp distance bound

Keep the current top operand’s relation tag and a first-value bit in finite control. Keep earlier operands, each with its own first-value bit, on one stack. On the first constant, push a special bottom sentinel and cache that constant with first=true. On a later constant, push the previous cached pair and cache the new constant with first=false. A unary operation updates the cached relation and keeps the stack. Join reads the one stack top, combines its relation with the cached relation, pops that top, and inherits its first bit. Joining when the top is the sentinel, or any sort error, rejects forever. Empty input rejects; acceptance is the same cached singleton/closed/true test.

The invariant is exact: when the abstract operand stack is v_1,…,v_n, control holds v_n’s relation and whether n=1, and the auxiliary stack holds a sentinel followed by v_1,…,v_(n-1), each with the first-value bit it had on insertion. Initialization and each of push, unary update and Join preserve it. No access below the one old stack top is needed by the source transition. In a rejecting sink one can keep pushing a dummy on constants, popping on Join (empty pop is allowed), and keeping on unary letters, so the action is determined by the input category on every word. This is a deterministic visibly pushdown recognizer, with final-state acceptance allowing a pending call.

It is exactly the finite one-stack source interface of the existing StackMachine and checked compiler. With s=1 that compiler gives degree one and native distance two, one append per unpadded opcode. It preserves the decoded semantic stack and control. This smaller construction does not assert the exact formula-DAG preservation of the two-record construction above.

The distance bound is sharp. Let E=Empty_empty and J=Join_empty. Restricting K_w to words E^+ J^* gives exactly

$$\{E^{n+1}J^n:n\ge0\}.$$

Distinct positive powers E^i,Ej are distinguished by the suffix J^(i-1): it leaves one value from E^i, while E^j either underflows or leaves more than one. Thus K_w is nonregular for every w, including w=0. The established distance-one regularity theorem excludes every distance-one scaffold for K_w, regardless of its finite degree, labels and control. Degree one is already the minimum positive degree in the scaffold model. This optimality is for recognition distance, not for formula-preserving storage or the growing-width information tradeoff.

6. Exact Turing-machine timing and the transfer route

Define the two-letter block encoding e(o)=o#, where # is a fresh clock symbol, and extend e by concatenation.

Theorem 6 (strict TM realization and transfer). For each fixed w there is a deterministic one-work-tape strict real-time TM recognizing exactly e(K_w), and hence a degree-two, distance-two scaffold for that same encoded language.

This explicit padding prevents any hidden compression of internal work.

The work tape is initially entirely blank. The blank cell at position zero serves as Bottom; there is no prewritten special marker. The stack occupies consecutive cells to its right. Its symbols are (S,R,first), where first indicates that this is the first value above Bottom. Between blocks the head scans the top cell, or Bottom on an empty stack. Finite control records phase, a pending operand when needed, and the current acceptance flag. Initially the head is at position zero, phase is ready, and acceptance is false. A blank seen in ready phase means an empty stack by the invariant; blanks reached during a push are handled by the distinct pending phase.

• Constant opcode: read whether the current cell is Bottom, remember the chosen finite constant symbol and its first flag, preserve the scanned cell and move right. The # transition writes the new symbol at that cell, commits its acceptance flag and returns to ready phase.
• Unary opcode: if a correctly typed value is scanned, replace it using the finite table, preserving first. The # transition stays in place, commits acceptance and returns to ready. Otherwise reject.
• Join opcode: require a value with first=false, remember it in finite control, erase its cell to blank and move left. The # transition reads the left operand, checks equal sorts, writes their intersection while preserving that cell’s first flag, stays, commits acceptance and returns to ready.
• A # in ready phase, an opcode during the pending clock phase, underflow or a sort error enters a permanent rejecting state. Pending phases never accept.

Every action reads and writes at most the scanned cell and moves at most one position. Here the ordinary TM move alphabet includes staying in place. There is exactly one global transition per input letter and no endmarker or cleanup transition. Induction on complete blocks proves the tape-stack and postfix summary-stack agree. Intermediate phases reject, so truncated blocks are not accepted. The first bit detects singleton height without an unbounded counter. This TM preserves the semantic evaluation stack; unlike the immutable client it does not claim to retain a version of each overwritten tape stack.

The existing strict transfer theorem T89 therefore gives a degree-two, distance-two scaffold recognizing e(K_w), with the same acceptance on every prefix. This uses one tape and a finite alphabet for each fixed w. The source TM construction here has a written proof and finite corroboration; the generic transfer is the previously machine-checked theorem. Its source definitions MultiTapeMachine and initTape require all-blank initialization, and Move includes left, right and stay, exactly as used here. No new Lean verification of this SAT evaluator is claimed.

The two languages K_w and e(K_w) have deliberately different encodings. Neither is automatically the usual raw-formula language. The direct record compiler recognizes K_w; the exact TM route recognizes e(K_w). The usual scaffold-to-PEG step gives PEGs for K_w reversed and e(K_w) reversed, respectively. Neither transfer erases the padding, proves a reverse simulation, or supplies a new SAT complexity collapse.

7. What is sufficient, necessary, and still unknown

The results separate three questions that are easy to conflate:

• Lemma 1 and Theorem 2 identify the exact future-facing information and count how large it can be.
• Theorems 3 and 3a give necessary local-view and information-access tradeoffs; Theorem 3b shows that a short interactive transcript need not imply a small complete summary.
• Theorems 4-6 give sufficient fixed-width implementations. Only the stated recognition-distance bound is optimal; no optimality is claimed for their other access, alphabet or allocation bounds.

Horn SAT is the key comparison. Static satisfiability is tractable, yet its boundary relation may contain exponentially much information. Its closure protocol communicates only polynomially many bits, but each party may inspect its entire fragment to produce the next closure. The unresolved question is the cost of realizing those closure steps on immutable data with retained versions as the boundary width grows. Any answer must state the representation, preprocessing, variable naming and total-work model; a short transcript alone does not supply a constant-work closure oracle.

8. Literature, dependencies and verification scope

The relation operations are standard CSP semantics. Allender, Bauland, Immerman, Schnoor and Vollmer’s refinement of Schaefer’s theorem provides the Boolean constraint and polymorphism setting. Static tractability of Horn constraints is also explicit in Dowling and Gallier’s linear-time Horn algorithms, whose representation assumptions should be retained when quoting running time. Our counting arguments are supplied in full and do not import an unverified complexity separation.

Theorem 3a uses the classical deterministic set-disjointness obstruction. Sherstov’s author-hosted Thirty-Five Years of Set Disjointness, Section 2, states the rectangle and fooling-set method and applies the pairs (X,complement X). We reproduce that elementary argument and add the explicit opaque-pointer simulation contract. The Horn protocol uses ordinary least-model closure and monotone progress; its local computational cost is deliberately not replaced by its communication count. Novelty of this application and comparison has not been established.

Width-based constraint dynamic programming predates this note. Samer and Szeider’s parameterized #SAT paper explains primal versus incidence treewidth and proves an incidence-width algorithm. Its tables also track clause information and its counting arithmetic is not our Boolean finite-label model. We use the elementary primal-boundary Boolean construction, not their numeric complexity bound or integer-cost assumption.

Darwiche and Marquis’s A Knowledge Compilation Map, Sections 3-5 and Definition 5.6, already separates representation succinctness, queries and transformations including conjunction and forgetting. That is the closest established conceptual framework for this comparison. This note adds explicit boundary quotients and local persistent resource accounting to those familiar distinctions; it does not invent knowledge compilation. Our counts are not claimed to improve known Boolean-function counting bounds.

The syntactic-algebra note, the reviewed record compiler, and the TM transfer audit are the internal dependencies. The native radius is one more than the old endpoint radius; the reversal occurs only at scaffold-to-PEG transfer. No queue, deque, Schaefer dichotomy proof, P!=NP hypothesis or speculative lower bound is needed for the written theorems here. No generalized pumping result is inferred.

The finite checker and recorded output cover small exact relation tables, clause gadgets, retained DAG histories, slot permutations, Horn closure, disjointness fooling pairs, and the record, stack and tape evaluators used above. It counts read paths and copied old targets, rechecks retained stacks, and starts the tape evaluator from an all-blank tape. The output records bounds, shared components, omissions and source hashes. These finite experiments corroborate the constructions but do not prove the universal theorems or establish novelty; the unbounded claims rest on the written arguments.