Reversible restoration forces group memory

Research note, 30 September 2026. Written proof, not proof-assistant verified. The theorem concerns a typed, legal hidden-stack protocol and the finite summary channel inside a local realization. It does not claim that an entire pushdown stack can always be erased. Classical ingredients and the closest comparison found are credited in Section 8. Novelty is not established.

1. The reversible test case

The preceding supplied-summary theorem asks whether a particular finite monoid value can be restored after a pop. Its positive parity example and negative set-of-labels example suggest a sharper principle. Parity is reversible: toggling the bit can be undone. Set union is not: after adding a label, the current set does not say whether that label was already present.

This note isolates that distinction in a natural limiting case. A hidden frame can be pushed and later popped, the driver supplies the frame type on the matching pop, and the finite summary must update without reading the discarded frame or its predecessor. When every hidden word is permitted, finite restoration is possible exactly for permutation memory. Equivalently, the retained transition monoid is a finite group.

This is a representation-independent statement inside the stated summary interface. It applies to every finite summary set and every choice of update tables, not only to monoid morphisms supplied in advance.

2. Model and quantifiers

Let H be a finite nonempty alphabet of hidden frame types. Hidden stacks are words in H*, written top first. The protocol supplies two operations for each h in H:

• push_h changes w to hw;
• pop_h changes hw back to w.

Only legal, correctly typed pops are submitted. Thus the theorem concerns restoration of retained information, not detection of an empty stack or an incorrect pop label. Those observations are considered separately below.

A finite reversible summary consists of a finite set S, a surjective map

$$\sigma:H^*\longrightarrow S, \tag{1}$$

and total finite tables U_h,D_h:S -> S such that, for every w in H*,

$$\sigma(hw)=U_h(\sigma(w)),\qquad \sigma(w)=D_h(\sigma(hw)). \tag{2}$$

Surjectivity merely replaces S by the states actually realized by stacks. The tables use only the current finite summary and the supplied frame type. They have no concrete tail pointer, predecessor graph, scan, saved version or history oracle. Initialization is the fixed state sigma(epsilon). A hidden push or pop performs no allocation in this summary channel.

For a finite observation set Omega, a stack observation f:H* -> Omega is preserved when there is a table lambda:S -> Omega with

$$f=\lambda\circ\sigma. \tag{3}$$

A finite tuple of observations is handled by taking their product.

3. The group-forcing theorem

Theorem 1 (full reversible cone). Every update U_h in a finite reversible summary is a permutation of S, and D_h=U_h^{-1}. Consequently the transition monoid generated by the hidden pushes is a finite group of permutations. Conversely, any finite permutation action of H on S, with D_h=U_h^{-1}, defines a finite reversible summary on the orbit of the initial state.

Proof. Equation (2) gives

$$D_hU_h=\operatorname{id}_S. \tag{4}$$

Thus U_h is injective. An injective self-map of a finite set is bijective, so D_h is its inverse. The generated transformations are permutations. A finite submonoid of a group is a group: if a permutation has order k, its inverse is its positive power k-1, which already lies in the generated monoid. The converse follows by evaluating the product of the supplied permutations along the stack word. QED.

The proof identifies the obstruction precisely. A finite update may merge old summary states during push, but then no local pop can recover which old state preceded the merge. Finiteness turns the required left inverse into a full inverse.

4. Intrinsic residual characterization

Theorem 1 describes a supplied summary. The following criterion asks whether some finite locally reversible summary preserves a specified observation. Define the left residual equivalence of f by

$$u\equiv_f v \quad\Longleftrightarrow\quad f(zu)=f(zv)\text{ for every }z\in H^*. \tag{5}$$

It is a left congruence: u equiv_f v implies hu equiv_f hv. Say it is left cancellative when the converse also holds for every h:

$$hu\equiv_f hv\Longrightarrow u\equiv_f v. \tag{6}$$

Theorem 2 (reversible residual theorem). A finite reversible summary preserving f exists if and only if:

1. equiv_f has finite index; and
2. equiv_f is left cancellative.

When these conditions hold, the residual classes form the unique minimal summary up to isomorphism. Its size is the index of equiv_f; each hidden push permutes those classes and the matching pop applies the inverse permutation. Hence the theorem is both a characterization and an optimum state bound, not merely a construction bound.

Sufficiency. On the finite quotient, define

$$U_h([w])=[hw]. \tag{7}$$

Left congruence makes this well defined. Left cancellation makes U_h injective, and finiteness makes it a permutation. Set D_h=U_h^{-1} and read f(w) from [w]; the empty continuation in (5) makes that output well defined.

Necessity and minimality. Any preserving summary gives a finite permutation Moore machine by Theorem 1. Its behavioral quotient is exactly the residual quotient (5), the usual Myhill-Nerode construction in the top-first orientation. It is finite and no larger than the supplied summary. Its generator maps remain injective. Concretely, if U_h has order k and U_h(m) and U_h(n) have identical future observations, prepend zh^(k-1) to cancel U_h before any requested continuation z; then m and n also have identical future observations. This proves (6). Every preserving summary therefore maps onto the residual quotient, proving the lower bound and uniqueness. QED.

Effective form

If f is supplied by a finite Moore machine in the same top-first prefix orientation, minimize it and inspect each generator transition. The criterion holds exactly when every generator acts injectively on the reachable minimal states. This is a finite test. The theorem does not assert decidability when f is given by an arbitrary program or by an unrestricted pushdown specification.

5. Untyped pop collapses the content

Suppose a pop does not reveal which hidden label is removed, so one common table D must satisfy

$$DU_h=\operatorname{id}_S \quad(h\in H). \tag{8}$$

Every U_h is a permutation and has inverse D. Therefore all U_h are the same permutation U=D^{-1}.

Corollary 3 (untyped collapse). On the realized orbit, every finite summary satisfying (8) depends only on stack height modulo the period of U. It cannot retain any distinction between frame labels. Conversely, height modulo any fixed positive integer has such a summary.

If exact emptiness is also an observation, no finite summary exists. For the period p of the initial state,

$$\sigma(\epsilon)=\sigma(h^p), \tag{9}$$

although one stack is empty and the other is not. Likewise, if pop enabledness or the complete hidden top sequence must be preserved, the full stack cannot be erased into finite control. These are additional observation requirements, not consequences of restoration alone.

6. Metric reading

Give the finite residual quotient the discrete metric and pull it back to stacks:

[ d_f(u,v)=0u_f v, d_f(u,v)=1.

On a reversible cone, every push_h and matching pop_h is an isometry of this quotient. In particular,

[ d_f(hu,hv)=d_f(u,v).

This is stronger than a one-sided Lipschitz estimate. A push cannot contract a distinction that a later pop must reconstruct. The algebraic cancellation law is the zero-distance form of that metric statement.

This concerns one fixed summary interface and its selected observations. It does not identify raw stored graphs under arbitrary future scaffold contexts.

7. Boundary examples

Parity passes

For one hidden label X, let f(w) be the parity of |w|. The two residual classes are exchanged by pushing X; the same exchange performs the pop. The memory is the group Z/2Z. This explains structurally why the previous parity restoration example succeeds.

More generally, length modulo k is retained by a k-cycle. These are positive examples, not a claim that group memory can recover the full stack.

Presence and emptiness fail

For f(w) = 1 when X occurs, pushing X maps both the absent and present classes to present. The minimal transition is not injective. This is the same irreversible merge exposed by the X versus XX set-summary witness.

For f(w) = 1 exactly when w is empty, every push merges the empty and nonempty residual classes into nonempty. Exact emptiness therefore cannot be maintained by a finite fully hidden reversible summary.

The earlier tag repair is outside the cone

The three-element rightmost-tag summary from the finite missing-bit example has an overwrite transition and is not a permutation summary. It succeeds there because the reachable presentation does not supply an arbitrary reversible hidden cone: only seven configurations and a restricted operation pattern are relevant, and the stack labels remain projected. The present theorem correctly does not reject that construction.

Retaining structure changes the model

A visible shadow frame, saved predecessor pointer or predecessor graph can restore non-group information by reading retained structure. That may be a valid persistent representation, but it is not finite-control restoration under (1)-(2). Likewise bounded private runs, control states that carry the old value, and restricted reachability can evade the full-cone hypothesis.

8. Relation to established work and novelty

The residual construction is the classical Myhill-Nerode theorem, applied in the top-first orientation. Permutation automata and pure-group languages are classical; see Gabriel Thierrin, Permutation automata, and Robert McNaughton, The loop complexity of pure-group events. Later reversible-automata work studies which regular languages admit reversible recognizers and their state complexity. The finite-set step “left inverse implies permutation” is elementary.

The additional contribution here is the precise restoration model, its equivalence to left-cancellative stack residuals, the minimal-summary bound, and the separation between typed restoration, untyped collapse, and exact stack-legality observations. This connects the earlier local-erasure theorem to classical permutation automata. It may be a useful formulation, but novelty is not established.

9. Verification and consequence for persistent compilation

The executable checker minimizes finite Moore machines and checks the residual transitions. It verifies that parity and length modulo three are permutation summaries, while presence, emptiness and the rightmost-tag observation fail injectivity. It also exhaustively checks all common-pop tables on sets of size at most four and finds only solutions in which the two push tables coincide. See the recorded output.

These are exact finite checks of the stated examples and bounded exhaustive check. They do not prove the general theorems, analyze an unrestricted source program, build a scaffold or constitute proof-assistant verification.

Inside a passing erased-stack quotient, a group summary occupies only finite control and hidden pushes/pops allocate no logical record. If the remaining visible stack satisfies the earlier bounded-spread hypotheses, the established persistent compiler still yields degree two, native access distance two and one physical node per input. The scaffold preserves the same-word language; the PEG transfer introduces exactly one reversal.

The next question is whether a restricted-reachability analogue replaces permutations by a finite groupoid or partial bijection system, and whether its least residual object is effective for deterministic visibly structured sources. That is the point where control assistance and visible stack boundaries must be represented explicitly rather than hidden in terminology.