Run 08: the exact simultaneous-record compiler interface

Date: 23 September 2026

Result

The direct and causal batch compilers have the same valid core construction. The exact whole-run theorem is the following.

Let a bounded simultaneous record transducer have s roots, at most A fresh records per input letter, q pointer fields per record, and old-address radius r. Suppose:

1. its initial roots are missing or point into one fixed finite, immutable, pointer-closed record graph;
2. its transition plan is determined by finite control, the input letter, and bounded labelled rooted unfoldings of the old roots;
3. it does not branch on physical pointer identity; and
4. each new root and field targets missing, a bounded old address, or a slot in the current simultaneous batch.

Then it compiles exactly and letter-synchronously into a scaffolding automaton of degree

$$d=\max\{1,s+Aq\}$$

and observation/update distance at most r+1.

The proof is the direct paper’s tuple-packing construction with its virtual initial table. Fixed initial records are finite decoder data. A dynamic logical pointer is a physical scaffold node plus a finite slot tag. A root edge and at most r field edges recover an old target. Every fresh target uses SELF plus its slot tag. The virtual base case and the one-step commuting square give the whole run by induction.

The maximum with one is required only by the native convention that scaffold degree is positive. It changes nothing when s+Aq>0.

Observation factorization

The no-identity clause is not incidental. For any fixed encoding and distance k, the action of a scaffolding automaton factors through

$$(\text{control},\text{input letter},N_k),$$

where N_k is the native rooted neighbourhood. Hence a source transition can be implemented through that encoding only if configurations with the same triple require the same scaffold action. Conversely, any finite legal action function on those triples is a scaffolding transition table. This is the exact local interface between a source program and the target automaton.

Physical alias identity does not factor through native views. Consider a root whose two ports point either to one old leaf twice or to two distinct but behaviorally identical old leaves. The native rooted views agree at every depth, but the pointer-equality predicate differs. No scaffold transition can branch on that predicate unless the presentation stores the needed distinction in finite labels or another observable coordinate.

This does not mean the compiler destroys aliasing. If one fixed source plan copies both old addresses, the compiled port words reach the same physical endpoint in the shared case and two endpoints in the split case. The compiler preserves aliases supplied by the source graph; it cannot discover alias identity as extra control information.

Paper alignment

Direct palindrome paper

Definition 10.1 and Theorem 10.2 already state all four hypotheses, the virtual-table base case, and max{1,s+Aq}. The whole-client normalization theorem separately excludes identity tests. No correction follows from this run.

Causal scaffold algebra

Definition 9.1 already excludes branching on physical pointer identity, and the proof of Theorem 9.2 gives the correct dynamic tuple-packing step. Two boundary clauses remain to be added in a future coordinated edition:

• state the fixed virtual initial-graph case, or restrict the theorem to missing initial roots; and
• write max{1,s+Aq}, or explicitly assume s+Aq>0.

With those clauses, the theorem is complete by the argument above. This is a local statement repair, not a counterexample to simultaneous-batch compilation. Proposition 9.5 inherits the chosen initialization convention for whole runs. Its local feedback and same-step-cycle argument survives.

Transfer and unary papers

The transfer construction initializes empty stacks from the native base. The unary paper begins with the native base history. Neither uses the record compiler’s virtual initial heap. This result therefore changes no theorem in those papers.

Executable evidence

check_compiler_interface.py checks:

• an explicit shared-versus-duplicated alias witness through native depth eight;
• every pair of root targets over missing, base, and two bisimilar leaves through depth five;
• preservation of shared and split endpoints by a fixed copied-address plan;
• the current direct and causal statement markers; and
• the earlier virtual-initialization audit of 117 initial configurations, 4,095 first steps, and 143,325 two-step executions.

The finite checks corroborate the boundary cases. The factorization and compiler arguments above supply the general statements.

Disposition

R03 is complete. The future causal edition needs two short compiler clauses; the direct theorem remains the aligned reference statement. No circulated paper body or PDF was changed.

The next review package is R05: strict timing, reversal, and empty-input handling in the transfer proof, followed by the remaining unary guard dependencies.