Bounded disagreement, stored feedback, and local observation

Research note, 30 September 2026. Written proofs with classical dependencies; no proof-assistant verification or priority claim.

The question and a concrete example

Suppose several possible computations disagree a little about when to push or pop a stack. Can one maintained stack organize all of them, even when its own next action depends on information retained in that stack?

Consider a machine that pushes on a, then pops on b until empty, and thereafter pushes on b. On a^n b^m its height is |n-m|. Deciding when to start growing again uses the stored empty-stack test. A finite controller whose actions depend only on its input history cannot track this height by a reflected counter within any constant error. Nevertheless, an immutable stack implements the machine directly.

Now make each operation occupy two input positions, a. or b., and allow a nondeterministic source to perform that operation either at its letter or at its following dot. Different runs have different heights between the two positions. They agree at each pair boundary and never differ from the machine that acts early by more than one. The dots here belong to the specified example language; the compiler below inserts no letters.

The construction absorbs that bounded disagreement in finite control, then stores the reference stack and the deterministic summary in the same linked stack. This gives both an observation guarantee and an explicit maintenance cost. Those are separate requirements: metric continuity alone does not pay for constructing the new memory.

1. Model and quantified contract

All machines have finite alphabets and control. A source P is a real-time nondeterministic pushdown machine with a finite nonempty initial-state set and initially empty stack. One transition consumes one letter, reads its control and top symbol or emptiness, and pushes one symbol, pops one symbol, or leaves the stack unchanged. There are no epsilon steps or top rewrites. A pop at empty is either disabled or explicitly a no-op. Rules may be partial. Acceptance is existential finite-control acceptance, optionally with a top/empty predicate. Every finite legal run counts, including rejecting runs and prefixes of runs that later get stuck.

A supplied observer D has the same normalized operations, one initial state, and is deterministic and complete: every control/top-or-empty/input combination has exactly one rule. It reads its own stack when choosing an action. It cannot inspect the source run. Let h_rho(w) and h_D(w) denote the respective stack heights, excluding the bottom sentinel.

For a supplied integer B >= 0, the hypothesis is

$$\forall w\in\Sigma^*\ \forall\rho\in\operatorname{Runs}_P(w), \qquad |h_\rho(w)-h_D(w)|\le B. \tag{1}$$

Theorem 1 (supplied stack observer). Condition (1) is decidable from the finite descriptions of P,D,B. A failure yields a finite word and legal source run witnessing the first exit. If (1) holds, an effective construction gives a complete deterministic real-time unit-stack machine M with

$$L(M)=L(P),\qquad h_M(w)=h_D(w)\quad(w\in\Sigma^*).$$

The equality of languages holds at every input cut, including the empty word. M has a strict persistent implementation with one logical root, one pointer field per record, and at most one fresh logical record per letter. The reviewed record compiler gives a degree-two, native-distance-two scaffold appending exactly one physical node per letter. Its language is L(P); the scaffold-to-PEG transfer gives L(P)^R.

These are construction bounds, not optima. The finite control and label alphabets depend on P,D,B. The theorem does not decide whether an unspecified observer or unspecified bound exists. It is a sufficient certificate for a specified presentation, not a characterization of every persistent language.

2. Paying for the observer: synchronized composition

For each input letter, annotate it by the observer’s actual stack action: c for push, r for a pop from a nonempty stack, and i for no change. In particular, a nominal pop that does nothing at empty receives i. Write the resulting word over Sigma x {c,r,i} as eta_D(w). Its visible height is exactly h_D(w), and it has no return from visible height zero.

Pairing lemma. Given a visibly pushdown machine A over this annotated alphabet, its execution on eta_D(w) and D’s execution on w can be implemented by a single pushdown machine over the original alphabet. Its control is a pair, and each stack frame is a pair of stack symbols.

Proof. Both stacks start empty. Inspect their paired top, or joint emptiness. The D rule selects the annotation and its new control. Feed the annotated letter to A. A call pushes the two new symbols as one pair; a return pops one pair; an internal step keeps the paired stack. Thus both projections remain exactly the component stacks. A may be nondeterministic or partial; its missing branches simply have no product transition. If both components are deterministic and complete, the product is too. This proves the claim by induction on input length.

For verification only, the same lemma holds with an arbitrary nondeterministic, possibly partial, reference pushdown T: choose one of its legal rules, derive that rule’s annotation, and take the paired transition. Product runs then correspond to a reference run and a compatible annotated A run. This is not closure of arbitrary two-stack products. The shared push/pop schedule is the reason only one stack is needed.

3. The finite buffer and first-exit checker

Use the buffer normalization from bounded-stack-skew.md, now on the annotated alphabet. The source reads the original input component; the annotation supplies the visible action. This constructs machines on all annotated words, without requiring the annotations to be realizable by D.

Here is the invariant needed from that construction. At visible height H, write a source stack bottom to top as s = vu, where

$$C=\max(0,H-B-1),\quad |v|=C,\quad |u|\le 2B+1.$$

The visible stack has H frames. The first min(H,B+1) have dummy payloads; the rest store v. Finite control stores the source control, u, and t=min(H,B+2). Each frame also stores the old cap t, to restore it on pop. When the source stack is nonempty, u is nonempty and contains its top. The extra one-cell margin is essential for source top tests on visible calls and internal letters, which cannot inspect the visible stack.

Apply the source operation to u, obtaining u_0; let delta h be its actual height change. For the actual visible change delta H, compute

$$e'=|u|-\min(t,B+1)+\delta h-\delta H. \tag{2}$$

This uses finite control only. If |e'| <= B, normalize as follows. A call below the core threshold pushes a dummy; above it, move the first symbol of u_0 onto the visible stack. A return from a real frame prepends its payload to u_0; a dummy return adds nothing. An internal step keeps the stack. The old cap on a popped frame restores the new cap. The invariant proves both directions of source-run correspondence, exactly as in the earlier note. Before determinization there is a source stack decoder.

The finite state bound for this simulation, before auxiliary acceptance flags, is

$$|Q_P|(B+3)\sum_{j=0}^{2B+1}|\Gamma_P|^j,$$

with at most (B+3)(|Gamma_P|+1) frame symbols. Source top/empty acceptance is already a finite-control predicate because it can read u.

Construct two visibly pushdown machines. V_B discards a transition when (2) exits the interval and otherwise retains source acceptance. E_B instead enters an accepting error state at that first exit. On the error step and afterward it still performs the prescribed visible action, using arbitrary dummy payloads when pushing. Consequently it can still be paired with D.

Compose D with E_B by the pairing lemma. This is a finite pushdown machine. Before the first exit its invariant decodes a real source run; every actual first exit is represented. Therefore its language is nonempty exactly when (1) fails. Pushdown emptiness decides the condition. Standard pushdown-to-grammar conversion and shortest derivations give a shortest violating word; retained source-rule tags recover its run. The first-exit construction uses P,D,B directly and does not assume the desired bound.

The nondeterministic-reference version also decides a supplied pairwise bound: compose one copy of P as reference with E_B for a second copy. An accepted word has two legal source runs with height difference greater than B at some prefix, and conversely. This works even when P is partial.

4. Determinization and persistent realization

Assume the checker finds no exit. On eta_D(w), every legal source run is represented in V_B and no additional source run is introduced. Hence

$$w\in L(P)\quad\Longleftrightarrow\quad \eta_D(w)\in L(V_B).$$

Apply the corrected Alur-Madhusudan visibly pushdown determinization to V_B, obtaining W. Complete it if needed with rejecting behavior that continues to obey the visible stack discipline. The pairing lemma applied to D,W gives the deterministic machine M in Theorem 1. Undefined source prefixes reject; the completed observer and summary continue to operate.

Store the paired stack as immutable cons records. A push allocates one record labelled by the paired symbol and pointing to the old root. A pop copies the top record’s tail, and a keep copies the root. Control and the top label or empty test choose the rule. There is no hidden scan or post-input work. With one root, one field, allocation at most one, and old address radius one, the reviewed interface has

$$s=A=q=1,\quad r=1,\quad d=\max(1,s+Aq)=2,\quad k=r+1=2.$$

Initialize with an empty logical stack and the fixed initial controls; the compiler’s fixed virtual initialization supplies the representation without an inserted input letter. Old records are never mutated. The scaffold preserves the decoded D and W stacks and their controls at every cut. The whole construction preserves the original source’s existential future acceptance. It does not retain one chosen nondeterministic source history, reconstruct every past execution, or preserve the original graph’s ports and labels under arbitrary testing contexts. No physical identity test occurs.

5. An intrinsic condition for complete sources

Call P complete if every control/top-or-empty/input combination has at least one rule. Select an initial state and a single rule for each such combination. This finite syntactic choice defines a complete deterministic observer D whose run is a legal run of P on every word. No future-input oracle or successful-run selection is involved.

Let the height diameter and the radius about this selected run be

$$\Delta(P)=\sup_{w,\rho,\sigma} |h_\rho(w)-h_\sigma(w)|,\qquad R_D(P)=\sup_{w,\rho}|h_\rho(w)-h_D(w)|,$$

with all runs starting in the specified initial configurations. Suprema may be infinite. Since the selected run is one of the runs, and by the ordinary triangle inequality on integer heights,

$$R_D(P)\le\Delta(P)\le2R_D(P). \tag{3}$$

Corollary 2 (bounded spread). For complete normalized P, finite pairwise height diameter is equivalent to finite radius about any syntactically selected deterministic run. If a bound Delta(P) <= B is supplied, it can be checked by the pairwise first-exit construction and implies the persistent realization of Theorem 1. Thus bounded perturbation of the common-height condition suffices for determinization and strict persistent compilation.

This is an intrinsic property of all runs of the given complete machine, independent of which deterministic selector is chosen. It is not invariant under replacement by an arbitrary language-equivalent presentation. The equivalence in (3) characterizes bounded run-height spread, not all bounded persistent realizations. It does not decide existence of an unspecified B.

The factor two can be attained. On each of the first two input letters let P choose push or keep, and thereafter keep forever. Choose the reference to push on the first letter and keep on the second. Its radius is one; after two letters the possible heights are 0,1,2, with diameter two. Completeness matters for this selector proof: a selected branch in a partial machine can die while other source branches continue. Totalizing a partial source can also change its height diameter.

6. Local observation has an explicit modulus

Consider any complete deterministic unit-stack machine with acceptance in finite control, including M. A configuration consists of finite control and its stack word, read top first. Pad the end of a finite stack with an infinite sequence of a distinguished missing symbol. Let V_m(x) be the control and first m symbols of that padded word, for m >= 0.

Define d(x,y)=0 when the configurations agree, and otherwise

$$d(x,y)=2^{-j},\qquad j=\min\{m\ge0:V_m(x)\ne V_m(y)\}.$$

Nested prefix agreement proves the ultrametric inequality

$$d(x,z)\le\max\{d(x,y),d(y,z)\}.$$

This is the elementary prefix ultrametric on decoded configurations, not a new metric construction and not a metric on physical node identities. For every input letter a, its update F_a satisfies

$$V_{m+1}(x)=V_{m+1}(y) \ \Longrightarrow\ V_m(F_a x)=V_m(F_a y), \tag{4}$$

for every m >= 0. Equal control and top/empty choose the same rule. A push adds the same symbol, a keep preserves the shared prefix, and a pop discards at most one common symbol. This proves (4), including the empty case. Equivalently, d(F_a x,F_a y) <= 2 d(x,y). Iteration yields

$$d(F_w x,F_w y)\le2^{|w|}d(x,y).$$

In epsilon-delta language, for horizon t and tolerance epsilon > 0, delta=epsilon/2^t suffices uniformly over words of length at most t. More concretely, agreement of V_t guarantees the same finite-control acceptance after every continuation of at most t letters. These answers are exact, not probabilistic or approximate acceptance decisions.

The height comparison in (3) and the prefix metric here are different measurements. The first lets a bounded buffer align histories; the second bounds how quickly a fixed controller can expose a hidden stack difference. Neither is claimed to be the minimal language-residual metric. Configurations with different stored stacks may still have identical future acceptance. The metric uses decoded endpoints, including missing. Native scaffold views need the reviewed extra frontier layer; no same-radius native/endpoint identity is assumed.

7. Why a metric bound alone is insufficient

Fix a literal representation: each bit of a finite word is the label of one immutable unary record, and its one pointer is the next record. The last pointer is missing. Consider complementing every bit while preserving the word length. This map is an isometry for the prefix metric: the first disagreement and the position of termination do not change.

Yet on a heap containing just an n-node all-zero chain, its exact all-one output requires at least n new records. No old record has the required label. A terminating chain of length n needs n distinct records, since revisiting one would create a nonterminating cycle. Thus there is no uniform allocation bound for this operation in this literal immutable encoding, even though it has the strongest possible continuity modulus. A fixed finite initial reserve changes the lower bound by at most a fixed constant.

This is deliberately not representation independent. Store a polarity bit with the root and decode each label by exclusive-or with that bit; then complementing the represented word only toggles the polarity. This alternative encoding preserves decoded word behavior but changes raw graph observations. It illustrates precisely why choosing and maintaining the representation is part of the theorem, beyond controlling observation distance.

8. Positive and negative tests of scope

For the two-position valley example in the opening, a complete observer acts on a or b and keeps on the following dot. Unexpected protocol symbols enter a dead control and keep the stack. The source allows only legal pair prefixes; at each first position it independently chooses early or late, remembering a pending operation in finite control if necessary. It also enforces a* b* at pair boundaries. Every legal branch is within one of the observer, and zero fails on the first delayed a. Acceptance at pair boundaries with empty stack gives

$$\{(a.)^n(b.)^n:n\ge0\}.$$

This genuinely nondeterministic source has unbounded stack depth and repeated timing choices. The theorem supplies an implementation without treating the observer’s stack feedback as free advice.

No finite reflected input-only clock tracks all its legal runs. Fix n and let the number of b. pairs tend to infinity. The true height eventually grows by one per pair. Therefore the eventual finite-state clock cycle under the repeated block b. must have mean signed increment one per pair. There are finitely many starting clock states, so the signed increment over m such blocks is m+O(1), uniformly for states reachable after (a.)^n. After (a.)^n, a putative bounded-error clock starts at least at n-B. Reflection can only increase its height relative to the unreflected sum. After n further b. blocks its height is at least 2n-B-O(1), while the source height is zero, a contradiction. This excludes the earlier reflected clock model, not absolute signed-sum advice, arbitrary observers, or other representations on this specified block protocol.

For a negative source condition, let a complete unary source independently push or keep on every letter, and make all states reject. At length n its possible heights range from zero to n. Its diameter is unbounded and no observer can be within a fixed bound of all those runs. Its accepted language is empty and has a finite-state implementation. Thus failure of the height condition cannot imply a language-level persistent-memory obstruction.

9. Established ingredients and additional work

• Nowotka and Srba, Height-Deterministic Pushdown Automata (MFCS 2007), Theorems 3 and 4: synchronized products and real-time height-deterministic determinization are established. Their theorem preserves exact height synchronization. The zero-disagreement case is therefore classical.
• Mahajan, Meyer and Nimbhorkar, On the Complexity of Membership and Counting in Height-Deterministic Pushdown Automata, Section 4.1, Proposition 3: complete deterministic pushdown transducers already provide height advice for real-time height-deterministic machines. Allowing a stored stack to direct height is not itself a new idea. Their advice convention uses absolute integer sums; our observer is charged for its actual stack, and our earlier negative example uses reflection.
• Alur and Madhusudan, Adding Nesting Structure to Words, corrected author version, Theorem 3.3 and the visible translation: determinization is imported, not reproved by experiments. The author version explicitly repairs the earlier determinization construction.
• Immutable cons stacks and retaining old roots are standard persistent data structures. The Lab’s reviewed bounded-record compiler supplies the strict scaffold bounds and initialization contract; it is not an appeal to a general amortized persistence theorem. See foundational-contracts.md for the persistent data-structure, pointer-machine, residual/bisimulation and transfer sources.

The additional argument here combines the existing bounded buffer with stored-feedback pairing, a first-exit checker for supplied and pairwise bounds, and an intrinsic bounded-spread corollary for complete sources. The observation modulus and the encoding-specific allocation counterexample separate semantic stability from operational cost. These are incremental working results; their literature novelty is unestablished. No new language class beyond real-time deterministic pushdown languages is claimed. The stack case gives a controlled testbed for a broader principle, not that broader principle yet.

10. Verification and the next mathematical issue

The proof is a written invariant and composition argument using the cited classical theorems. The accompanying finite checker and recorded scope test local pairing, buffer decoding, first exits, the early/late example and the observation estimate on specified finite domains. They do not implement a VPA determinizer, pushdown emptiness, the scaffold compiler, or a proof assistant, and do not certify the universal statements by enumeration.

The useful next question is whether bounded disagreement can be measured at the memory actually exposed to future computation, rather than at every source run’s full stack height. The all-rejecting example shows why the full height condition can demand irrelevant information. A concrete next test is to erase designated private frames under a supplied finite label projection. First ask for a checkable transition-congruence condition: do equal projected configurations give equal projected successors and acceptance, one input letter at a time? A private top-symbol guard can break that condition even when projected heights agree. If the condition holds, determine how to maintain access to the next exposed frame with immutable shortcuts, and whether the bounded-buffer proof applies to that projected machine. A long erased segment is a test of the access contract, not an impossibility for every encoding. Merely bounding projected heights without controlling the effect of private information would not justify the extension.