Pumping certificates and the missing recurrence theorem

Research note, version 7, 24 September 2026.

Overview

A pumping proof must do two different jobs. It must show that a chosen piece of a computation can be repeated safely, and it must show that every long enough accepted computation contains such a piece. Native scaffolds make the first job surprisingly concrete: equality of complete rooted observations can be certified by a finite bisimulation and then preserved under every common continuation. But growing persistent graphs need not revisit that equivalence class, even when the language itself is regular. A safe repeat therefore does not provide a recurrence theorem.

Visible stacks show what the missing structure looks like. Suppose one word segment pushes a fixed frame above an arbitrary old stack tail, a middle segment runs without exposing that tail, and a second segment removes the same frame. Repeating both outer segments pumps the computation even though the first segment is not a loop. The repeatable object is a typed operation on an unbounded parameter, not a repeated complete configuration.

This note develops three boundaries around that example:

1. A bounded live behavioral quotient is exactly enough to recover ordinary finite-state pumping. Every nonregular scaffold presentation must escape that bounded-state regime.
2. A well-quasi-order gives one-sided pumping in monotone systems, but exact destructive observations block this route for unbounded stacks and for nonregular scaffold presentations with monotone port traversal.
3. A paired-retraction law captures the algebra of push, middle computation, and matching pop. It proves pumping soundness once the interface is found, but it does not force that interface to recur.

The tree, visibly pushdown, and well-structured-system ingredients are classical. The contribution here is a synthesis at the scaffold boundary, with explicit finite certificates and counterexamples. The open problem is to find an intrinsic nonregular scaffold condition that guarantees recurring typed graph contexts without first translating the machine into a known grammar class.

Finite-interface pumping schema

The common source of the regular and context-free pumping lemmas is a typed derivation tree. Suppose a compositional derivation system has a finite type set T. Every node has bounded rank, contributes a bounded terminal fragment, and a subtree may be replaced by any subtree of the same type. Assume also that every proper parent-to-child context contributes at least one terminal.

If a derivation has a root-to-leaf path longer than |T|, two nodes on that path have the same type. Write the entire tree as C[K[t]], where K is the nontrivial one-hole context between those nodes. Type preservation makes every

$$C[K^j[t]] \qquad (j\ge 0)$$

a valid derivation. If the yield of C is u[ ]z and the yield of K is v[ ]y, the resulting words are

$$uv^jxy^jz,$$

where x is the yield of t and |vy|>0. Bounded rank turns sufficiently large word length into sufficiently large tree height. For rank at most b>1, at most c terminals per node, and m types, a derivation with no repeated type on a path has at most (b^m-1)/(b-1) nodes and at most c times that many terminals.

This is the classical pumping lemma for recognizable tree languages, applied to derivation trees. A DFA is the unary case, with states as types. A context-free grammar uses nonterminals as types. The important object is not a repeated substring or a repeated complete machine state. It is a repeatable one-hole context with a finite boundary type.

Visible stacks supply a nonregular positive case

Alur and Madhusudan’s visibly pushdown grammars use finitely many variables and productions of the forms

$$X\to\epsilon,\qquad X\to aY,\qquad X\to aYbZ,$$

with the last form pairing a visible call a and return b. These derivation trees have rank at most two and contribute at most two terminals per node. For a reduced grammar with m variables, the safe bound p=2^{m+2} therefore suffices: every generated word w with |w|>=p has

$$w=uvxyz,\qquad |vy|>0,\qquad |vxy|\le p,$$

and uv^jxyjz is generated for every j>=0. The displayed bound is deliberately loose; the point is the interface, not constant optimization.

For a well-matched visibly pushdown language, the repeated variable is a stack-context type. One wing v may build a finite frame above an arbitrary old stack tail, and the other wing y later discharges the corresponding frame. Repeating both wings never inspects or copies the opaque tail. A horizontal repetition is the special case in which one wing is empty.

Under the persistent-stack scaffold compiler, each extra copy allocates new nodes, so complete rooted graphs still need not recur. What recurs is the typed operation on a stack parameter. This is the concrete nonregular subclass missing from version 1: visible stack structure turns classical parse-tree recurrence into a finitely checkable scaffold cut interface.

A sound, finite certificate

Fix a deterministic native scaffolding automaton M. After a prefix u, write C(u)=(q_u,G_u,r_u) for its finite control and rooted persistent graph. The unlabelled base and a missing endpoint are distinct observations. Write C(u) ~ C(v) if q_u=q_v and the rooted graphs have equal full labelled port unfoldings. This does not require equal graph sizes or allocation times.

A finite bisimulation certificate is a relation between nodes of the two graphs, with an added missing sink on each side. It must contain the root pair, preserve labels (including base and missing), and relate corresponding successors at every ordered port. Starting at the roots and closing under matched successors checks the condition in at most O(d(|G_u|+1)(|G_v|+1)) operations. No pointer-identity test is used by M.

Certificate principle. If y is nonempty and C(x) ~ C(xy), then for every integer j>=0 and every suffix z,

$$M(xy^jz)=M(xz).$$

In particular, acceptance of xyz certifies acceptance of xy^jz for all j>=0.

Proof. Equal full unfoldings give equal native observations at every finite radius. Equal controls and the same input letter therefore select the same update row and next control. Corresponding old-address port words reach related endpoints, fresh self-pointers are paired with each other, and missing endpoints remain paired. Adjoin the two fresh roots to the old bisimulation relation. This proves preservation by one input step, hence by every common word. Since reading y returns to the same equivalence class, induction on j, followed by the common suffix z, proves the formula. The case j=0 is included. QED.

Native views collapse base and missing at radius zero. The argument above uses full unfoldings, so it does not rely on the same-radius identification addressed in the scaffold proof review’s Run 07.

Why matching a fixed-radius view is insufficient

Fix any radius r. Make two unary chains with the same r+1 top labels and different labels immediately below them. Their native radius-r views agree. A distance-two cursor can copy the old successor’s label and outgoing port into a new root, thereby advancing one old link per input symbol. After r+1 cursor steps the different buried labels are exposed. A finite control can record the exposed bit, so acceptance can differ too.

Thus a one-step observation is not automatically a substitutable interface: future navigation can expose distinctions outside the initial view.

Why even full equivalence need never recur

Consider the one-state, degree-one archival automaton over a unary input alphabet. Its single state is accepting. Every input symbol appends a node labelled 0 with its port pointing to the previous root. Distance one suffices. The machine recognizes every word.

At input length n, its root is a chain of n zero-labelled nodes ending at the unlabelled base. If n<m, the port word of length n reaches the base in the first graph and a zero-labelled node in the second. Hence no two distinct cuts have equal full unfoldings.

The language is regular and has ordinary pumping, but this particular presentation never has the certificate above. Full graph equivalence preserves behavior under arbitrary scaffold continuations. Recognition needs only the continuations that this fixed controller actually performs. The distinction is not a defect of bisimulation: it shows the difference between preserving an archive and preserving the answers of its client.

A finite-summary trap

Suppose reachable configurations admit a summary sigma into a finite set S, with sigma(C after a)=f_a(sigma(C)) for every input letter and with acceptance determined by sigma(C). Then the summaries themselves form a DFA for L(M). This is the classical finite-congruence argument.

Therefore a finite, update-closed summary of complete configurations cannot characterize nonregular scaffold languages. A useful extension must allow structured contexts, parameters, or unboundedly many interfaces. In a context-free pumping argument, the repeated nonterminal types a derivation context, not the entire pushdown configuration.

Live records cannot be resurrected

For a scaffold configuration C, let R(C) be the physical nodes reachable from the current root by port paths. If reading one letter changes C to C’, then

$$R(C')\cap V(C)\subseteq R(C).$$

Indeed, every old endpoint installed in the fresh root is obtained by following a port word from the old root. Existing old edges never change. Every old node subsequently reachable from the fresh root is therefore already reachable from the old root. By induction, once a physical record leaves the live set, no later update can recover it.

This is stronger than saying that an unqueried coordinate was irrelevant to one completed run. It is a permanent future statement at the cut. Physical allocation may grow forever while the part that can still affect any future answer stays small.

Bounded live quotients recover regular pumping

Let F(C) be the canonical minimal residual figure from FPRD-T129: first keep the rooted reachable graph, then identify nodes with equal full labelled port unfoldings. Consider a fixed scaffold automaton with q controls, g working labels, and degree d.

Live-quotient criterion. Suppose there is B>=1 such that

$$|F(C(w))|\le B \qquad\text{for every input prefix }w.$$

Then the recognized language is regular. One explicit, deliberately loose DFA-state bound is

$$N_B=q\sum_{b=1}^{B} b(g+1)^b(b+1)^{db}.$$

Consequently every accepted word of length at least N_B has a factorization w=xyz with |xy|<=N_B, |y|>0, and

$$xy^jz\in L\qquad(j\ge0).$$

Proof. For a figure with b nodes, overcount its descriptions by choosing the root in b ways, each label in g+1 ways including the distinguished base, and each of d ordered successors as one of b nodes or missing. Multiply by q and sum over b<=B. Thus there are at most N_B possible pairs of control and rooted figure.

FPRD-T129 says equal figures are preserved by every common scaffold update. They also expose the same finite view, so the fixed controller selects the same next row and control. The finite set of reachable control-figure pairs is therefore a DFA quotient. The displayed pumping statement is the ordinary repeated-state proof applied to that quotient. QED.

The condition is presentation-dependent, but it gives an exact language characterization:

$$L\text{ is regular} \quad\Longleftrightarrow\quad L\text{ has a scaffold presentation with uniformly bounded }|F(C(w))|.$$

The reverse implication is the criterion. For the forward implication, put a DFA for L in finite control and let every input allocate the same one-node self-loop figure. Thus B=1 suffices. The accept-all archival chain above shows why the statement must say has a presentation: another presentation of the same regular language may retain an unbounded live quotient.

In particular, every scaffold presentation of a nonregular language has unbounded minimal residual figures. This is the point where a generalized pumping lemma must stop looking for a bounded complete state. Visible stacks cross the boundary by repeating a finite operation type over an unbounded stack-tail parameter.

WQO pumping: recurrence without deletion

There is a second classical route beyond repeated equality. Let X be the configuration set of a deterministic word transition system over a finite alphabet, ordered by a well-quasi-order <=. Assume every letter action is monotone and the accepting set is upward closed.

WQO one-sided pumping theorem. There is a number P such that every accepted word w with |w|>=P has a factorization w=xyz satisfying

$$|xy|\le P,qquad |y|>0,qquad xy^jz\in L\quad(j\ge1).$$

Proof. Call a word bad when the configurations reached by all its prefixes contain no pair C_i<=C_j with i<j. Bad words form a prefix-closed, finitely branching tree. If they had unbounded length, Konig’s lemma would give an infinite branch, contradicting the well-quasi-order. Hence there is a uniform P beyond which some C_i<=C_j occurs, with j<=P.

Put x before the first cut, y between the cuts, and z after the second cut. If T is the transition induced by y, then C_i<=T(C_i). Monotonicity gives

$$T(C_i)\le T^2(C_i)\le T^3(C_i)\le\cdots.$$

Applying the monotone suffix z preserves this chain. Its first endpoint is accepting, so upward closure makes every later endpoint accepting. QED.

The missing j=0 case is essential. A strict comparison C_i<C_j only says that the later state covers the earlier one; it does not justify deleting the growth. If C_i and C_j are equivalent under the quasi-order, then C_j<=C_i also holds, the zero-copy case follows, and the ordinary j>=0 pumping law is recovered. Finite-state pumping is exactly this equivalence case.

A WQO alone proves existence of P, not a usable numeric bound. Effective WSTS theory adds computable transition and predecessor hypotheses. Quantitative length-function theorems bound controlled bad sequences, often at very high complexity.

This gives FPRD a precise next test. A genuine scaffold extension order must be a WQO, preserve every letter update monotonically, and make acceptance upward closed. Ordinary graph inclusion is not enough: adding an edge can change a native missing-versus-present observation and send the controller to a different row. The order must express presentation-specific opaque growth, such as extension below a protected stack interface. No such order is claimed here for unrestricted scaffolding automata.

Separating destructors obstruct structural WQOs

The stack proof is an instance of a general observation theorem. Let X be a configuration set, let $o:X\to O$ be a finite observation, and let D be a finite family of total destructive probes $d:X\to X$. Partial probes are made total by adjoining a distinguished missing configuration. For a probe word $w\in D^*$, write $d_w$ for its composite, and define

$$x\equiv_D y \quad\Longleftrightarrow\quad o(d_w(x))=o(d_w(y))\text{ for every }w\in D^*.$$

Thus $\equiv_D$ is equality of complete observable probe trees.

Destructor-separation obstruction. Suppose a preorder $\preceq$ preserves observations and makes every probe monotone:

$$x\preceq y\Longrightarrow o(x)=o(y), \qquad x\preceq y\Longrightarrow d(x)\preceq d(y) \quad(d\in D).$$

Then

$$x\preceq y\quad\Longrightarrow\quad x\equiv_D y.$$

Consequently, if X has infinitely many $\equiv_D$-classes, no such preorder can be a WQO.

Proof. Monotonicity gives $d_w(x)\preceq d_w(y)$ for every probe word w. Observation preservation then gives equal observations after every w, which is exactly $x\equiv_D y$. Choosing one representative from each of infinitely many equivalence classes produces an infinite sequence with no comparable pair. QED.

For stacks, D contains pop and the complete observation trace separates exact stack words, recovering the version 6 theorem. For a rooted labelled port graph, D contains one successor probe for each port, with a missing sink. The complete probe tree is precisely the full labelled port unfolding, so $\equiv_D$ is the bisimulation equivalence used by FPRD-T129.

It follows that a scaffold presentation with infinitely many minimal residual figures cannot carry a WQO that both preserves exact native node observations and makes every port traversal monotone. By the version 3 characterization, every presentation of a nonregular scaffold language has infinitely many such figures. Therefore this structural WQO route cannot prove pumping for a nonregular scaffold language.

The scope is exact. This does not rule out an order tailored directly to whole input updates, an order using deliberately coarser observations, or a paired context whose inner records remain opaque until a matching retraction. It says that exact observational navigation cannot simultaneously separate all residual figures and order them upward.

Exact stack observation obstructs a WQO

The WQO theorem does not subsume ordinary stack pumping when the stack is observed exactly. Let stacks be finite words over a nonempty alphabet, with the top at the left. Write obs(s) for the top symbol, using a separate value for the empty stack, and let pop remove the top symbol while fixing empty.

Exact-stack WQO obstruction. Suppose a preorder $\preceq$ satisfies

1. $s\preceq t$ implies $\operatorname{obs}(s)=\operatorname{obs}(t)$;
2. pop is monotone: $s\preceq t$ implies $\operatorname{pop}(s)\preceq\operatorname{pop}(t)$.

Then

$$s\preceq t\quad\Longrightarrow\quad s=t.$$

Consequently, on the infinite set of finite stacks, $\preceq$ cannot be a well-quasi-order.

Proof. Monotonicity iterates, so $s\preceq t$ implies $\operatorname{pop}^k(s)\preceq\operatorname{pop}^k(t)$ for every k. Observation preservation therefore makes the complete sequences

$$\bigl(\operatorname{obs}(\operatorname{pop}^k(s))\bigr)_{k\ge0} \quad\text{and}\quad \bigl(\operatorname{obs}(\operatorname{pop}^k(t))\bigr)_{k\ge0}$$

identical. This sequence reads every stack symbol and then the empty marker, so it uniquely determines the stack. Hence s=t. An infinite sequence of distinct stacks is then a bad sequence, contradicting the WQO property. QED.

Push monotonicity is not needed. The obstruction already follows from exact observation and pop. Both hypotheses matter: if exact observation is dropped, unary stacks ordered by height form a pop-monotone WQO; if pop monotonicity is dropped, equality of the current top observation is a finite-class WQO.

This explains why visible-stack pumping uses a paired context rather than a single upward comparison. A larger stack is not safely above a smaller one under every future pop: repeated returns eventually expose the exact depth and symbols that differ. The later pumping wing must discharge precisely the frames introduced by the earlier wing before the outer continuation resumes. For scaffolds, the analogous lesson is that a useful order must protect an opaque interface whose hidden growth the permitted continuation cannot later expose one record at a time.

Paired retraction: pumping without a loop

The visible-stack example admits a sharper machine-level formulation. Work in any deterministic continuation quotient Q: equal elements have the same acceptance and remain equal after every common suffix. Let V, X, and Y be the transformations induced by three words v, x, and y. Fix the quotient element c reached after a prefix u.

Paired-retraction pumping theorem. Suppose

$$Y\circ X\circ V(p)=X(p)$$

for every p in the forward orbit $\{c,V(c),V^2(c),\ldots\}$. Then for every j>=0,

$$Y^j\circ X\circ V^j(c)=X(c).$$

Consequently, for every suffix z, the word

$$uv^jxy^jz$$

has exactly the same acceptance as uxz for all j>=0.

Proof. The case j=0 is immediate. For the induction step, associativity and the orbit law give

$$\begin{aligned} Y^{j+1}X V^{j+1}(c) &=Y^j\bigl(YXV\bigr)V^j(c)\\ &=Y^jX V^j(c)\\ &=X(c). \end{aligned}$$

The common suffix z preserves equality in the continuation quotient. QED.

This separates two roles often conflated in a pumping proof. V may push a frame, open a recursive call, or otherwise move to a genuinely different and larger configuration. It need not return to c. Y cancels that one move only after the intervening computation X, and it must do so uniformly at every deeper parameter reached by another V. A conventional loop is the degenerate case where the parameter does not move.

Checking the law only at c is insufficient. On the three-element carrier, let V send 0 to 1 and 1 to 2, let X be the identity, and let Y send 1 to 0 while fixing 0 and 2. Then YXV(0)=X(0), but two copies finish at 2 rather than 0. The invariant is the law over the entire V-orbit, not one successful cancellation.

For a finite quotient orbit, the certificate is checked by visiting each orbit element once. A persistent stack has an infinite orbit, but the law can still have a finite proof: represent p as an opaque tail, V as adding one fixed frame, and Y as removing that frame after X. This is the algebraic content of the typed one-hole context in the visible-stack construction. It supplies pumping soundness once such an interface is found; a separate recurrence theorem must still force one to occur in every sufficiently long accepted computation.

LMR’s boundary and the next question

LMR’s Theorem 21 forbids a total computable procedure producing a longer accepted word from every sufficiently long accepted word of every total PEG. It is not confined to repeating substrings. A universal, effective recurrence theorem strong enough to supply such a procedure cannot hold. Our finite certificate does not contradict this: checking a supplied segment does not guarantee that any qualifying segment exists.

The next precise question is: can a nonregular scaffold subclass admit finitely checkable, parameterized cut interfaces with a proved recurrence property? Visible-stack scaffolds now give one affirmative subclass, by the classical grammar/tree argument above. The open problem is to identify a larger intrinsic scaffold condition that guarantees a finite family of typed graph contexts without first translating the machine back into a known grammar class.

Evidence and sources

The checkers exercise finite instances of every construction and sharpness example below. They corroborate the formulas and implementations but do not replace the unrestricted tree, WQO, recurrence, or scaffold arguments.

• Bisimulation and fixed-view limits: 327 degree-one graphs, 106,929 ordered pairs, 118,030 common-row extensions, 59,015 native-view comparisons, 528 archival-cut pairs, 17 buried-label examples, and 1,143 repeated-block/suffix comparisons.

• Finite interfaces and visible stacks: 16,739 finite-type paths, 1,619 two-bracket Dyck derivation trees through five pairs, 15,508 extracted one-hole contexts, 77,540 pumped words, and 4,080 nested two-wing words.

• Live quotients: 2,327 degree-one histories with 77 minimal figures, 23,270 no-resurrection instances, 22,500 quotient-extension comparisons, five counting strata, and 2,520 pumped words in a growing-allocation parity recognizer with live quotient size one.

• WQO pumping: every pair of monotone actions on finite chains through size four, covering 1,004,550 pumped computations and the zero-copy, nonmonotone-update, and non-upward-acceptance failures.

• Paired retraction: all 19,748 transformation triples on carriers through size three, with nine pump exponents and every suffix transformation for each qualifying orbit, plus the smallest base-only failure.

• Exact stacks: every ordered pair of stacks over alphabets through size three and heights through six, including both examples obtained by dropping one hypothesis.

• Separating destructors: every preorder and binary-observation destructor system through four states, with two independent destructors through three states. Every comparable pair remained in one complete probe-trace class.

• Loff, Moreira, and Reis, The computational power of parsing expression grammars, Theorem 16 and Definition 20/Theorem 21: https://arxiv.org/html/1902.08272v2#S5.S2.

• FPRD-T129, Future-context full abstraction and canonical residual figures: https://fprd-lab.joshgay.chatgpt.site/claims/FPRD-T129.

• Native-observation convention, scaffold proof review Run 07: https://fprd-lab.joshgay.chatgpt.site/research-programs/scaffold-proof-review#native-observation-shift.

• Comon, Dauchet, Gilleron, Jacquemard, Lugiez, Loding, Tison, and Tommasi, Tree Automata Techniques and Applications, Section 1.2: https://jacquema.gitlabpages.inria.fr/files/tata.pdf.

• Alur and Madhusudan, Visibly Pushdown Languages, Definition 4 and Theorem 6: https://www.cis.upenn.edu/~alur/Stoc04.pdf.

• Finkel and Schnoebelen, Well-structured transition systems everywhere!: https://www.cmi.ac.in/~madhavan/courses/concurrency2017/literature/finkel-schnoebelen-wsts.pdf.

• Schmitz, Complexity hierarchies beyond elementary; controlled bad sequences and length-function bounds: https://arxiv.org/pdf/1312.5686.

Version history

1. Initial research note: certificate soundness, two limitations, and the finite-summary boundary. No circulated manuscript or PDF was revised.
2. Added the classical finite-interface schema and its visible-stack instantiation, with a separate bounded checker. No circulated manuscript or PDF was revised.
3. Added no-resurrection, the bounded live-quotient regularity criterion with an explicit DFA and pumping bound, and its exact presentation-level characterization of regular languages. No circulated manuscript or PDF was revised.
4. Added the WQO one-sided pumping theorem, the exact zero-copy boundary, and the compatibility requirements for a future scaffold order. No circulated manuscript or PDF was revised.
5. Added the paired-retraction pumping theorem, its orbit-wide hypothesis, and a counterexample to checking only the first cancellation. No circulated manuscript or PDF was revised.
6. Added the exact-stack WQO obstruction and sharpness examples. No circulated manuscript or PDF was revised.
7. Generalized the obstruction to separating destructor families and applied it to exact scaffold port navigation. No circulated manuscript or PDF was revised.