Safe Horn reassociation and the exact cost of eager synchronization

1 October 2026. Written proofs with finite executable corroboration; novelty unestablished. This continues compositional Horn Join.

Model and question

Use that note’s deterministic persistent Horn engine, prepared finite Horn3CNF leaves, fixed common boundary B, explicit length-l bit names, and positive Pin and Join operations. Private variables are distinct by unfolded leaf occurrence. Initialization and leaf indexes are charged as in the preceding construction; this note starts from completed, consistent handles. Public observations are satisfiability and least forced boundary facts for the represented formula. The exact syntax DAG is retained separately. Conditional internal engines are not public formula handles. No retraction, forgetting, name-identity oracle, or arbitrary-context graph equivalence is asserted.

Can balancing the evaluation tree reduce its propagation term D? We answer this for the stated eager synchronization algorithm, not for every possible representation of Horn semantics.

Lemma 1: saturated boundary assumptions can be rebased

Let F be a finite Horn formula, S a set of positive boundary facts, and M the least model of consistent F and S. Put Z = M intersect B. Then

least(F and S) = least(F and Z).

Proof. S is contained in Z, so every model of F and Z models F and S. Conversely M itself models F and Z. The two inclusions between least models prove equality. No enumeration of Z is required to apply the semantic lemma. Operationally, a completed forward-chaining state for F and S already contains all facts of Z and has processed their antecedent occurrences. Reusing that state under Z requires neither counter changes nor rule replay. This claim uses the completed-state invariant, not merely equality of returned answers.

Proposition 2: local reassociation without closure recomputation

Consider a consistent quiescent evaluation node ((P,Q),R), under its current positive boundary assumptions S. P,Q,R may themselves be composite blocks; Pins internal to a block remain in that block’s formula. All participating engines have the same completed boundary set Z. Replace it by (P,(Q,R)), retaining the three block engines and sharing a completed cache representation of Z for the two new composite nodes. Keep the exact syntax handle unchanged.

This preserves the current least model and all future positive-Pin and Join answers of the whole handle. At a supplied root the replacement costs O(1) bounded-field reads and O(1) fresh records; it performs no closure events and no name traversal. Old versions are unchanged. At depth h, finding the node and rebuilding its immutable ancestor path costs O(h); no constant-cost arbitrary-node access is assumed. A global balancing operation must charge all its traversal and rotations separately.

Proof. By quiescence every child at every edge has boundary Z. Lemma 1 lets us view each block engine as completed under Z. Their least models then combine, since private namespaces are disjoint. The new Q,R composite under Z is already closed: neither child can add a boundary fact, and neither fails. The same holds for the new root. The combined assignment equals the original least assignment. For a later seed set U, every retained fact is a consequence of the unchanged whole formula with S and U. Forward chaining from these states is sound; its terminal synchronized model is the least extension, by the preceding Join proof. Induction gives preservation through any finite sequence of positive extensions and joins. The proof preserves occurrence bindings; regrouping does not identify private variables. The two replacement composites contain fixed-size child/cache pointers, proving the local cost. A fixed record encoding may use more than two physical records, still O(1).

The precondition is enforced by the operation protocol: only successful, drained solver states are eligible. It does not require traversing the tree to compare every cache. This proposition does not apply mid-propagation or claim a comparable cache invariant after failure.

Scope is essential. Take P = {x}, Q = {x implies y}, R empty. The regrouped Q,R engine knows x,y under Z, whereas unconditional Q and R forces neither. Exporting that engine as an unconditional Q-and-R handle is incorrect.

Theorem 3: an exact propagation identity

Fix a quiescent successful evaluation tree with I internal binary composition occurrences and boundary cache Z. Run the preceding eager algorithm on a positive Pin, with no topology changes during the operation. If it completes successfully with boundary Z’, then its number of internal pending pops is

D = I * |Z' minus Z|.

Proof. Initially every internal occurrence has cache Z, by recursive quiescence. Finally every internal occurrence has cache Z’, by the same invariant. Caches only grow. At each node each newly inserted boundary fact is queued once, and successful completion drains every queue. Thus each node pops exactly |Z’ minus Z| facts. Summing proves the identity. Repeated physical handles contribute their distinct evaluation occurrences. No premise relates I to the number of physical nodes in a compact syntax DAG.

For a successful fresh Join of two completed operands with internal occurrence counts I1,I2 and initial caches Z1,Z2, the corresponding identity is

D = |Z'| + I1 * |Z' minus Z1| + I2 * |Z' minus Z2|.

The new root starts empty; the same per-node counting proof applies. Failed operations may stop early and need not satisfy either equality.

Consequence and decisive research choice

A binary tree with m leaf occurrences has I=m-1 regardless of height. Hence rebalancing alone cannot reduce D for a successful Pin with the same resulting boundary delta. For m empty leaves and one fresh fact x, both a balanced tree and a chain have D=m-1 and m newly marked leaf facts. The closure itself is trivial. The cost comes from this engine’s eager duplication of boundary knowledge. For an already known fact the delta is empty and D=0, as required.

The bound from the previous note therefore specializes to

O((1+k+I*|Z' minus Z|+A+E)*(l+1))

for successful Pin. Balancing may improve depth, continuation space, or the cost of accessing a chosen subtree; it does not remove this broadcast term. This is an exact property of a specified algorithm, not a lower bound on all persistent Horn representations, scaffolding automata, or Turing machines.

This closes the proposed balancing route to reducing D. The useful next question is whether an engine can share inherited boundary facts and notify only rule-dependent subscribers while preserving old versions and exact root answers, with an explicit charge for routing and deferred work. Such a change requires a new invariant: the present one intentionally synchronizes every leaf, including leaves that contain no relevant rule. It is not enough to rename this work or hide it inside a query.

Established ingredients and additional argument

Least-model Horn propagation is classical; see Dowling and Gallier (1984). Lemma 1 is an elementary closure-operator fact. Persistent linked structures and the distinction between accessing a path and modifying a constant-size neighborhood are classical; see Driscoll, Sarnak, Sleator and Tarjan (1989), sections 1–2. We do not import their generic persistence bounds without their model hypotheses. Here the local construction directly allocates immutable replacement records. The additional argument is the conditional-state reuse contract and the exact event identity for our composite engine. Neither an independent novelty claim nor a new general Horn lower bound is established.

The prior transfer contract can compile these bounded local record steps. It cannot convert the identity into a machine-independent lower bound or make a whole Pin a single real-time input transition. Name traversal, initialization, and the operation clock remain charged. Any scaffold-to-PEG language statement still reverses the recognized language. No new transfer theorem is needed here.

Verification scope

Checker and recorded output check 186 consistent triples selected from six tiny programs, their 744 positive extensions, preservation of retained states, the conditional-export counterexample, and balanced/chain empty examples through 32 leaves. The oracle enumerates assignments for the small semantic examples. These are finite checks, not proofs of the quantified statements. Python sets and recursive calls do not verify bounded pointer access, concrete allocation constants, or formal machine compilation. The general results above are written mathematical proofs; no proof assistant was run.