Foundations: observations, compilation and normal forms

Consolidated working statements, 29 September 2026. These statements use the native Loff-Moreira-Reis model and the completed proof-review obligations. They do not replace the circulated editions.

Contents

1. Two different future quantifiers

Fix degree $d\geq1$ , a finite working alphabet, and rooted chronological scaffolds, with missing targets and the distinguished unlabelled base. The full unfolding records, for each finite port word, its working label, base endpoint, or missing endpoint.

Arbitrary-context graph behavior. Equal full unfoldings are exactly labelled bisimilarity. They are stable under a common legal row and therefore under every common sequence of rows. Unequal unfoldings have a finite distinguishing port word. A continuation with one cursor port per new node, and descriptors of length at most two, follows that word and exposes the distinction to a native radius-two observer.

Here the quantifier is over legal testing continuations, chosen for the distinction in question. It is not restricted to rows generated by the controller that originally built the graph. “Unary continuation” means one used cursor port in each new node, not a claim that the original degree is one.

One fixed controller. For a fixed deterministic machine $M$ , compare configurations by acceptance after all input suffixes under $M$ . Equality of control and full unfolding implies this equivalence. The converse fails: a controller that ignores its graph may give identical future answers on different unfoldings. For reachable prefixes this is the ordinary right residual equivalence of the recognized language.

Consequently a quotient by all graph observations and the minimal residual machine of a particular language are different objects. A graph-normal-form theorem is not automatically a language-minimality theorem, and language equivalence does not imply stored-graph equivalence.

2. The native finite-view convention

Let $P_m$ be the endpoint table through port-word length $m$ , retaining working label, base, and missing as distinct outcomes. Let $N_m$ be the native recursive LMR neighborhood. At remaining depth zero, base and missing both have the empty observation. Thus

$P_m(S)=P_m(T)\Rightarrow N_m(S)=N_m(T),\qquad N_{m+1}(S)=N_{m+1}(T)\Rightarrow P_m(S)=P_m(T).$

There is no general same-radius identity. At every depth jointly, the distinction disappears:

$(\forall m,\ N_m(S)=N_m(T))\iff \mathcal U_S=\mathcal U_T.$

The proof is recursive truncation in one direction and one extra layer at a base-versus-missing frontier in the other. This is the repair established in review run 07.

3. Bounded simultaneous-record compilation

The source is a deterministic finite-rule transducer with $s$ roots, finite record labels, $q$ pointer fields per record, at most $A$ fresh records per input letter, and bounded old-address radius $r$ . Its source observation must factor through the specified bounded labelled rooted unfolding, with the native observation convention aligned to that radius. It cannot branch on physical pointer equality.

Every new field and root names missing, an old address of length at most $r$ from a root, or a slot in the current simultaneous batch. Existing records are immutable. Initial roots are missing or point into one fixed finite immutable pointer-closed graph.

Under this interface, the reviewed compiler has

$d=\max(1,s+Aq),\qquad k=r+1.$

One physical node packs each fresh batch using finite slot tags. A root edge plus at most $r$ field edges names an old record. Fresh targets use SELF and a slot tag. Fixed initial records live in finite virtual decoder data, so no first-letter allocation charge or initialization letter is needed. The base case and the one-step commuting square give the whole-run result.

The compiler preserves decoded records, source roots, labels, copied aliases and deterministic control. It preserves same-word acceptance at every prefix. Its target graph has a different port and slot vocabulary; raw target-graph observations are not asserted to equal raw source-graph observations.

Copying aliases and observing identity are distinct. A shared leaf and two separate behaviorally identical leaves have equal unfoldings. A fixed copy plan preserves their endpoints but cannot choose its branch by discovering which presentation it received.

Use review run 08 and direct Draft 5, Definition 10.1 and Theorem 10.2, as the aligned contract. An implementation must bound both the decision observation and copied old addresses; a bound on addresses alone does not certify applicability.

4. The distance boundary and structural encoding

Result	Construction and guarantee	Boundary
Distance one is regular	The finite summary $(q,N_1)$ determines its successor summary. A DFA can use at most $q[1+(g+1)^{d+1}]$ states. Every DFA conversely uses a dummy-node scaffold.	Recognition under one fixed controller. Arbitrarily large stored graphs may remain distinguishable by other contexts.
Every finite distance reduces to two	For source degree $d$ and distance $k\geq2$ , add a shortcut for every nonempty source port word of length at most $k$ . Degree is $\sum_{\ell=1}^k d^\ell$ . Read the compiled radius-two view, not radius one, to reconstruct the source native view.	Same control, labels, one node per letter and prefix acceptance. Source edges are recovered by a decoder; additional shortcut ports change the raw graph vocabulary.
One working label and two controls suffice	Add $\lceil\log_2(1+gq)\rceil$ SELF/missing marker ports to the shortcut construction, reserving the zero code for the base. Decode label and source control in radius two. The two physical controls retain acceptance.	A finite-degree existence normal form, not an optimum or a graph-isomorphism theorem. Empty-prefix control is supplied separately by initialization.

For shortcut installation, a path from the new node either remains in SELF, becomes missing, or exits once into old storage by a descriptor $t$ and then follows a suffix $s$ . Old storage cannot return to the fresh node. The compiled old endpoint is therefore named by at most two shortcut hops, $[t][s]$ , omitting empty factors.

These facts give

$\mathsf{SA}_{\leq1}=\mathsf{REG} \subsetneq\mathsf{SA}_{\leq2}=\mathsf{SA}.$

The persistent coordinate-selector language from T159 witnesses strictness. The normal-form degree bounds are construction bounds, not lower bounds. None of these results changes the reversal in LMR’s theorem:

$L\in\mathsf{SA}\quad\Longleftrightarrow\quad L^R\in\mathsf{PEG}.$

5. Dependencies and assurance

Residual equivalence and graph bisimulation are established ingredients. Rutten’s Universal coalgebra: a theory of systems provides the general behavioral framework; the Lab supplies the native scaffold specialization and its explicit testing contexts. The residual tower organizes finite future observations; its mere existence is not a bounded-resource implementation.

Classical pointer-machine simulation and persistent-data-structure work motivate encodings, but their model assumptions cannot be silently imported: mutable edges, identity tests, amortized costs and multiple internal steps do not satisfy the simultaneous-record contract by themselves.

The review preserves the causal full-abstraction theorem with the native one-layer repair; it preserves the causal compiler with explicit virtual initialization and positive degree. It leaves the direct sequence application conditional on its sequence contract. The source-level sequence audit is not a complete compiler certificate or a proved numerical locality radius. The independent real-time-machine transfer retains its classical recognizer premise. These distinctions are recorded in the review checkpoint.

No new formal verification of these five foundations was performed in this run. Existing finite audits and imported formal results retain their stated scope. Circulated PDF and HTML paper bodies remain unchanged pending the coordinated revision process.

Primary references:

Loff, Moreira and Reis, The computational power of parsing expression grammars: https://arxiv.org/html/1902.08272v2.
Rutten, Universal coalgebra: a theory of systems: https://ir.cwi.nl/pub/48.
Schonhage, Storage Modification Machines: https://doi.org/10.1137/0209036.
Driscoll, Sarnak, Sleator and Tarjan, Making Data Structures Persistent: https://www.cs.cmu.edu/~sleator/papers/making-data-structures-persistent.pdf.

The current application is bounded stack-skew normalization.