Persistent Horn closure with charged local work

1 October 2026. Written construction and proof; novelty unestablished.

The question is whether the short Horn boundary protocol in SAT boundary dynamics can be implemented without hiding repeated expensive local closure computations. It can, for two fixed programs and subsequent positive seeds. Retaining truth and propagation counters makes each antecedent occurrence relevant at most once along a version lineage. Binary tries make the cost of names and immutable updates explicit.

1. Model and statement

A normalized Horn 3CNF program consists of rules A -> h, where A is a set of at most three variable names and h is a variable or false. If h is a variable, |A| <= 2. Drop tautologies h in A and remove duplicate body literals. There are n declared variables, m rules and p antecedent occurrences; put N = 1+n+m+p. For input requiring normalization, these size counts include the supplied rules and occurrences before any are discarded. An empty body is a fact, or an immediate contradiction if its head is false. Repeated rules may have distinct rule identifiers.

All variable and rule identifiers are explicit length-l bit strings, l >= 1, represented by immutable linked bit lists. Variable and rule namespaces are separate. The input supplies declarations, rule identifiers, and boundary flags. Duplicate declarations/rule identifiers and undeclared names are rejected. Equality is bitwise; there is no pointer-identity test, address arithmetic, unit-cost integer or hash oracle. For canonically numbered input, l = O(log(N+b+2)); arbitrary supplied names retain their actual length in the bound. Their conversion to canonical names is not free.

Records have a fixed finite set of labels and bounded outdegree. Every access follows a pointer from a held root; every allocation creates a constant-size immutable record. Record reads, bit reads, control steps and allocations are charged. Finite tuples can be encoded by a fixed number of binary records. Prepared program data are inputs of variable size, not fixed initialization. Preparation starts with empty maps and its cost is included below.

Theorem 1 (persistent positive extension). For every such fixed program P, independent preparation takes O(N(l+1)) time and fresh records. There is a fully persistent representation of its least-model closure under positive seed sets, with a distinguished inconsistent status. From any retained, consistent, quiescent version, processing k supplied seed names costs

O((k+a+e+1)(l+1))

in time and fresh records, where a is the number of newly marked variables and e the number of antecedent occurrences processed during that operation. Repeated seeds count in k. An inconsistent version stays inconsistent. Along any single version lineage, total newly marked variables are at most n and processed occurrences at most p. Thus preparation followed by K seed names in t nonempty or empty requests costs O((N+K+t)(l+1)).

The t term charges requests even when empty. It must not silently disappear from a bound advertised for an arbitrary operation sequence. The output observation is inconsistency, membership of a named variable, or an iterator of newly true boundary names. Membership costs O(l+1); materializing a whole assignment is charged separately. Inconsistent states expose only inconsistency, not a purported least model. All retained versions and program data are preserved.

This is a construction bound, not an optimum or characterization. P is fixed within each family of versions. Positive seeds are monotone; deletions, rule insertion and merging arbitrary program versions are not operations of this theorem.

2. Construction

Use a sparse binary trie of depth l, with an explicit missing-node marker, for each map. A lookup reads at most l+1 nodes. A put descends on the key, records the path in an immutable stack, and copies the path back to the root. It reads and allocates O(l+1) records, including temporary frames. No old node is overwritten. Leaves carry finite values or a pointer to a bounded tuple. Traversing an identifier also costs O(l+1).

The immutable program indexes are:

• variable name -> boundary flag and incidence list of rule identifiers;
• rule identifier -> body arity in {0,1,2,3} and head name or false;
• a list of zero-body rules.

Build these with trie lookups and puts from the explicit input. Each body has constant size, so normalization, declaration checks and incidence insertion cost O(l+1) per literal/rule. The indexes and input name lists use O(N(l+1)) records. No general sorting or random-access name table is assumed.

A version holds a truth trie (default false), a counter trie (default zero), and a conflict flag, together with the fixed program indexes. During an operation it also holds a work stack and a boundary-delta stack. Counters record processed true antecedents and take values in {0,1,2,3}.

mark(v):
    if truth[v] is false:
        truth := put(truth, v, true)
        push v on work
        if v is boundary: push v on delta

initialize:
    mark every fact head; fail on an empty false-headed rule
    drain work

extend(seed list):
    mark each seed; drain work

drain:
    while work is nonempty and conflict is false:
        pop v
        for rule j in incidence[v]:
            counter[j] := counter[j]+1
            if counter[j] equals arity[j]:
                if head[j] is false: set conflict
                else: mark(head[j])

The program rejects undeclared seed names by an index lookup before marking. The theorem concerns valid seed sequences; this check has the same cost. A failed operation may abandon the remaining work. It returns an absorbing inconsistent version; its partially processed counters are never reused as those of a consistent quiescent state.

3. Proof of Theorem 1

Maintain these invariants during draining:

1. Every marked variable follows from the program and the accumulated seeds.
2. Every marked variable is either processed exactly once or awaits that processing.
3. Each counter is the number of its body’s variables already processed.

Marking a seed preserves (1). Firing a rule preserves (1) because all its antecedents have been processed and hence are true. Truth lookup suppresses repeat insertion into work, proving (2). Distinct antecedents and the incidence lists prove (3); therefore a rule reaches its arity at most once. Zero-body rules are initialized once rather than waiting for an impossible incidence event.

If false fires, every satisfying assignment extending the seeds would make its body true, a contradiction. Otherwise, after draining, all marked variables are processed. Every rule with a true body has fired. Taking exactly the marked variables to be true is consequently a model extending the seeds. Invariant (1) makes it contained in every such model, so it is the least model. This handles unseeded cycles: a cycle alone proves no fact.

At a consistent quiescent state, new positive seeds preserve the old facts and counters. The same argument applies without restarting any incidence scan. Each mark attempt, index/counter operation, and work/delta action costs O(l+1). There are k initial attempts, at most a pops and at most e rule visits; at most one additional mark attempt per fired rule, hence at most e during extension. This proves the per-operation bound. Initialization also visits zero-body rules, covered by m in preparation. Summing (2) over a single lineage gives a <= n and e <= p for the total events, with one unit per request.

Trie path copying and immutable work cells preserve every old root. The proof therefore holds independently for extension of any retained version, not just the newest. It does not give one n+p event budget across a branching version tree. For a chain x1 -> x2 -> … -> xn, each separate extension of the empty-seed version by x1 processes n variables. r such branches cost Theta(rn) events in this construction; memoization across branches is not assumed.

4. Two-fragment composition without repeated rescanning

Let F and G be two independently prepared fixed programs with the same b boundary names. Their private names belong to disjoint semantic namespaces; local tries remain separate, so equal private bit strings do not identify variables across the fragments. Let N_F,N_G be their sizes. Use a common explicit name length l; if necessary, padding and corresponding input reading are charged in preparation. Neither side preprocesses jointly with the other.

Theorem 2 (charged Horn boundary composition). Least-model closure of F and G jointly, with shared boundary variables, can be computed on their persistent representations in

O((N_F+N_G+b)(l+1))

time and fresh records, including both preparations. It sends at most 2b boundary-name notifications. A retained consistent pair can be extended by positive boundary seeds. Along one lineage with K seed names in t requests, including the initial composition, the bound is

O((N_F+N_G+b+K+t)(l+1)).

For canonically numbered input this is a near-linear O((N_F+N_G+K+t) log(N_F+N_G+2)) construction. The bound covers one fixed pair of programs, not building an arbitrary expression of Join operations without rebuilding indexes. It computes joint satisfiability and the least assignment; it does not materialize the entire boundary relation.

Algorithm and proof. First close each side on its own facts. Whenever a side newly marks a boundary variable, place that name on a notification stack for the other side. Drain notifications by extending the receiving closure; append that side’s new boundary facts to the opposite stack. Initially send the deltas from both independent fact closures. An echo is harmless: the receiving truth trie suppresses duplicate marking. Subsequent external seeds are submitted to both sides. Stop on conflict or when both notification stacks are empty and the local engines are quiescent.

Each side marks each boundary variable once, hence at most 2b notifications along the whole lineage. Every derived fact follows from the union of programs and seeds. At termination the two local models agree on the boundary: any true boundary name has been delivered to the other side. Their union is a model, because the private namespaces are separate and each local model is closed under its own rules. It is contained in every model by the derivation invariant. A false-headed firing proves inconsistency as before.

A notification never restarts closure. Across all exchanges, Theorem 1 charges each side’s antecedent occurrence at most once. There are at most 2K external seed deliveries, 2b notifications and O(t+b) closure calls. This proves the bound, including calls that discover only duplicate facts. A stack work order suffices: the finite number of possible new facts guarantees termination; no queue amortization or fairness assumption is needed.

For example F contains x -> u and u -> y, where u is private; G contains fact x and y -> false. The first exchange carries x, F propagates to y, and the return exchange detects inconsistency in G. Both originally independent states remain available after this failed composition.

5. What this says about representational dynamics

The earlier boundary theorem says Horn fragments may have exponentially many bits of exact boundary-summary information. That does not force materializing that summary in order to solve one composition. Horn implication supports a monotone progress measure: a variable becomes true once on a lineage. This charges the local computation behind the short protocol, instead of treating closure as an oracle. It is an algorithmic sufficient condition for this operation interface, not a representation-independent lower bound for other interfaces or a new separation between complexity classes.

The elementary implementation uses finite-rule pointer primitives: inspect a root label, move a root to a child, copy a root, and allocate a binary cell from held roots. Bit-list traversal and explicit path stacks replace scalar loop indices and recursion. Counters remain finite because clauses have bounded arity. Each primitive has bounded local access and bounded allocation; the number of primitives for a full seed request is not bounded by a constant.

There is an important transfer obligation. The scaffold compiler in Foundational contracts requires fixed finite initialization and an input-step schedule. Prepared variable-size indexes cannot be silently installed in its initial graph. This note proves the pointer-data construction and its charged complexity, but supplies no complete serialized loader, clocked input language or verified microinstruction table. Therefore it claims no new raw Horn-SAT scaffold recognizer, strict real-time TM recognizer, numerical scaffold degree, or reverse scaffold-to-TM simulation. The next decisive step is to provide that loader and schedule with an explicit language and prove the compiler hypotheses. Any resulting PEG recognizes the reversal of the scaffold language, including its encoding and clock symbols.

6. Provenance, verification and open obligation

The forward-chaining mechanism is classical. Dowling and Gallier, Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae, Journal of Logic Programming (1984), give least-assignment algorithms using clause lists and counters. We add no new static linear-time Horn-SAT result. Our name-traversal and immutable-map costs are explicit extra charges.

Persistence is also established machinery. Driscoll, Sarnak, Sleator and Tarjan, Making Data Structures Persistent, JCSS 38 (1989), distinguish full from partial persistence and discuss path copying and stronger node-copying/splitting methods. We use elementary path copying; their stronger amortized bounds are not imported into our strictly immutable finite-label model without an implementation argument.

The additional result recorded here is the composition of those ingredients with the previous boundary protocol: an explicit per-lineage charged bound, separate private namespaces, preserved independent versions, and no repeated whole-fragment closure per exchange. Novelty of this combination is unestablished. It may be a useful specialization of known incremental inference techniques.

The companion checker and output test immutable trie updates, incremental closure, retained-version forks, and two-party exchange against independently enumerated satisfying assignments. They count trie reads/allocations and propagation events. Python control, static input normalization, tuple access, and integer test-harness names are not a certified pointer-machine implementation. The written proof supplies the asymptotic implementation argument. No Lean formalization or unrestricted theorem follows from finite tests.

Still open: the finite-alphabet loader and charged schedule needed for a concrete transfer corollary; whether the logarithmic immutable-map overhead can be reduced in this model; and operation interfaces permitting arbitrary fragment composition or retractions. Only the first is the immediate target.