Finite certificates that respect the bottom boundary

Research note, 30 September 2026. Written proof with an imported reachability theorem; no claim of literature novelty or proof-assistant verification.

1. Why heights, not just nominal actions, matter

A machine that chooses between pop and keep, starting empty, stays empty. The finite-cycle test nevertheless fails: it counts nominal pops even when the bottom boundary absorbs them. Similarly, a push enabled only at zero cannot repeat at positive height. Erasing this guard makes a bounded machine look unbounded.

Here we resolve these failures for one-counter sources: pushdown machines with just one kind of stack symbol. The certificate retains which pairs of source and clock heights may occur, including their boundary restrictions. Infinitely many pairs can have a finite description. For example, exact synchronization at arbitrary height is the ray (h,H)=(z,z), z>=0; the pop-or-keep example uses only its endpoint (0,0).

The result is an exact certificate characterization of bounded skew relative to a fixed clock in this subclass. It remains only a sufficient route to bounded persistent realization. It does not characterize all presentations or all languages admitting such a realization.

2. Models, observations and quantifiers

The source P has finite states Q, a nonempty initial set I, a finite alphabet Sigma and counter h initially zero. A rule (q,a,g,d,q’) consumes exactly one letter, where g is zero, positive or any, and d belongs to {-1,0,1}. If its guard holds at the old h, it sets h’=max(0,h+d). A pop that must be disabled at bottom has guard positive. A permitted pop at bottom is an explicit no-op under this convention. Nondeterministic rules are allowed; there are no epsilon steps, bulk updates or other counter tests. Acceptance is existential by a specified predicate on state and zero/nonzero counter.

Fix a complete deterministic input observer R with initial state r0, update tau(r,a), and output c(r,a) in {-1,0,1}. It cannot read the source state, source choice, or either height. Its reflected clock starts at H=0 and updates H’=max(0,H+c(r,a)). In particular, it is not the absolute value of a signed sum. Both machines read the same letters.

Bounded skew means

$$\exists B\in\mathbb N\ \forall w\in\Sigma^*\ \forall\rho \text{ a legal run of P on }w:\quad |h_\rho(w)-H(w)|\le B. \tag{1}$$

All finite legal runs count, including rejecting runs and prefixes of runs that later get stuck. The empty run counts for every initial state. This statement concerns a specified source and clock, not the source language under every possible presentation.

3. The certificate and its finite checks

Use coordinates

$$e=h-H,\qquad z=\min(h,H),\qquad (h,H)=(z+e^+,z+e^-),\quad e^+=\max(e,0),\ e^-=\max(-e,0). \tag{2}$$

A certificate has finitely many rows (q,r,e,A), with distinct (q,r,e). Here e is an integer and A is an ultimately periodic subset of the nonnegative integers. Its finite description is

$$A=F\cup\{z\ge T:z\bmod p\in D\}, \quad T\ge0,\ p\ge1,\ F\subseteq\{0,\ldots,T-1\},\ D\subseteq\{0,\ldots,p-1\}. \tag{3}$$

An omitted row means the empty set. A row denotes exactly the height pairs in (2) with z in A, at states q,r. The invariant need not be the exact reachable set. The checker does not assume reachability of any listed pair. Put B=max |e| over the nonempty rows. Initialization ensures there is at least one such row.

The obligations are as follows, for every row and every outgoing source rule on every letter. The new observer state is always tau(r,a).

Initialization. For each q in I, the row (q,r0,0) contains z=0.

Boundary. If 0 belongs to A, use h=e^+, H=e^- to test the actual source guard. For an enabled rule compute

$$u=\max(0,e^++d),\quad v=\max(0,e^-+c(r,a)),\quad e'=u-v,\quad z'=\min(u,v). \tag{4}$$

The target row (q’,tau(r,a),e’) must contain z’. Notice z=0 means at least one height is zero; it does not assert that both are zero or that the source is zero. In (4), z’ is either zero or one.

Interior. At z>0 both heights are positive. Ignore zero-only rules; any and positive guards are enabled. Put

$$e'=e+d-c(r,a),\quad t=\min(e^++d,e^-+c(r,a)). \tag{5}$$

Then t is in {-1,0,1}, and the obligation is

$$(A\cap\mathbb N_{>0})+t\ \subseteq A_{q',\tau(r,a),e'}. \tag{6}$$

This includes an interior step landing at z’=0. There is no clamping error: z>=1 and both unit decrements leave nonnegative heights.

These are effective finite checks on the supplied rules, clock and row descriptions. To check (6) against a row A’ with threshold T’ and period p’, set M=max(1,T,T’+1), L=lcm(p,p’). Check the implication z in A implies z+t in A’ for 1<=z<M+L. Below M this inspects the entire exceptional prefix. At and above M both membership predicates are periodic with period L, so one full period suffices. Empty target rows can use T’=0, p’=1, D’=empty. A failed inclusion has a concrete witness z. This is a decision algorithm for the infinite inclusion, not a sample-height test. No complexity or optimality claim is made for the possibly large period.

4. Characterization and proof

Theorem. For every source P and fixed observer/output table (R,c) of Section 2, (1) holds if and only if a certificate of Section 3 passes the initialization, boundary and interior checks. Every passing certificate establishes the bound given by its largest nonempty displacement. Conversely, if (1) holds with B, a passing certificate exists with displacements contained in [-B,B]. Thus the certificate bound need not be optimal, but restricting displacements to a supplied corridor loses no true instances.

Soundness. Induct on the input length of any legal run. Initialization places its starting pair in a row. If its z is zero, (4) is precisely the enabled transition and its target is included. Otherwise (5) follows by subtracting and taking the minimum of h+d and H+c. The source guard is handled correctly because h>0. Inclusion (6) puts the successor in its target row. Thus every reachable pair remains in the invariant, whose finitely many displacements have absolute value at most B. This proves (1) for all runs and prefixes, irrespective of acceptance.

Completeness. Suppose (1) holds with some B. This assumption is used only to prove that a finite certificate exists, not by its local checker. Form a system K_B whose finite modes are (q,r,e), -B<=e<=B, and whose single counter is z. At z=0 use exactly (4) for the enabled guards; at z>0 use (5) for any/positive guards. Omit transitions with e’ outside [-B,B]. Initial configurations are (q,r0,0;z=0), q in I. Keep the consumed letter as a transition label when comparing runs.

The coordinate map (2) gives a stepwise correspondence between K_B runs and source-clock runs that stay in this corridor. Both directions hold by (4)-(5); dropping an edge cannot introduce a run. Under the assumed bound, every original run stays in the corridor, so their reachable configurations correspond exactly.

K_B is an ordinary one-counter system with zero/positive guards and unit updates. To see that the imported pushdown theorem applies, encode z as A^z followed by a bottom marker. Positive increments, keeps and decrements replace the top A by AA, A or the empty word. A boundary update replaces the bottom marker by itself or by A followed by that marker. Guards select which rules are present. There is no rule that removes the bottom marker. Input labels can now be erased for configuration reachability.

The classical regular-post* theorem for pushdown systems gives an effectively constructible finite automaton for the configurations reachable from this finite initial set. We import this theorem, not a new saturation argument; a precise source is Schwoon’s Theorem 3.3, cited below. Restrict to a mode and remove the final bottom marker. The resulting language is unary regular. After determinization, its state sequence on A,A^2,… eventually repeats; hence its accepted lengths form an ultimately periodic set of the form (3).

For each mode use this exact reachable set of z values as its row. These rows contain the initial configurations. Any enabled original successor of a reachable configuration is reachable. By (1) it cannot leave the corridor, so it is also a K_B successor and belongs to a row. All local checks pass. This proves completeness, including bottom-only cycles and guard-restricted behavior. The regularity claim applies to K_B after bounding e, not to an arbitrary product of two unbounded counters. QED.

Effective consequences and limits

For a supplied B, K_B is a finite pushdown description, so the imported saturation construction computes candidate exact rows. Check every original transition for closure, including any that would leave the corridor. The test succeeds exactly when B is valid: if a run exits, its first predecessor is reachable within K_B and violates closure. This is another complete fixed-clock, fixed-bound test, consistent with the earlier first-exit VPA.

Without B, enumerate finite row descriptions and run the local checker. Completeness makes this a semidecision procedure for bounded skew for the fixed clock. One may also enumerate finite input clocks, with a supplied state budget or without one. If a suitable clock exists, a fair search finds a certificate. No terminating negative answer, bound on witness size, or decision procedure for unknown B follows from this argument. Repeatedly testing B=0,1,… already semidecided positive instances; the gain here is the finite certificate format, its completeness, and its exact treatment of guards, not a new positive decidability result.

5. Persistent compilation and what it preserves

A passing certificate produces (P,R,c,B) satisfying the hypothesis of the bounded-skew construction and its finite-state-clock extension. Annotate each input letter with the old observer state, normalize with a buffer of at most 2B+1 source symbols, apply visibly pushdown determinization, and compute that annotation online. This gives a deterministic real-time pushdown recognizer, with one unit stack action per original input letter.

Its immutable cons stack has one root, one pointer field per record, at most one fresh logical record per step, and access to the old root and tail. The reviewed simultaneous-record compiler therefore gives a scaffold of degree two and native distance two, allocating one physical node per input letter. Constants in its finite control and labels depend on the supplied source, clock and certificate. Empty logical stack uses a missing root; the compiler’s fixed virtual initialization and empty-prefix acceptance apply without an extra input symbol. These are construction bounds, not minimum resources. The certificate is checked before execution; its periodic sets are not queried by the running scaffold.

The scaffold accepts L(P) on the same words, including every prefix considered as a complete input. The scaffold-to-PEG transfer gives a PEG for L(P)^R. The decoded deterministic stack is preserved by the record compiler. Neither determinization nor this theorem preserves individual nondeterministic histories or the original stored graph’s behavior under arbitrary future testing contexts. The observation is acceptance under the fixed compiled controller. No general replay or context-adaptation guarantee follows.

6. Examples and a failed weaker format

Only bottom behavior. In one state choose pop or keep on x, both guarded any, starting empty. Use c(x)=0 and the single row e=0, A={0}. Formula (4) keeps both choices at (0,0); there is no interior obligation with a member. The certificate proves B=0. The previous zero-cycle test fails for every finite observer, because an eventual unary observer cycle permits abstract all-pop and all-keep paths with different nominal sums.

A guarded push once. Push on x only at zero and keep only when positive. With c(x)=0 use rows e=0,A={0} and e=1,A={0}. The former moves to the latter; the latter can only keep. This proves B=1 without treating the disabled push as a positive-height loop. This certificate is checked by the same rules, not by a special exception for bounded-height sources.

An unbounded, nonregular example. In one state over {a,b,x}, push on a at any height; pop on b only at positive height; on x keep at any height and additionally permit a nominal pop only at zero. Accept exactly at zero. Use c(a)=1,c(b)=-1,c(x)=0. The single row e=0,A=N passes: a and b move along the diagonal, while the extra x-pop acts only at its endpoint. Thus B=0 despite unbounded height. The accepted language is the one-bracket Dyck language with x letters ignored. Its intersection with ab is {a^n b^n}, so it is nonregular. The old guard-erased test still fails for every finite observer: its x-only subgraph has the same nominal pop/keep obstruction. This example connects the boundary repair to an actual nonregular scaffold application, though that language and its usual stack recognizer are classical.

Periodic rows. Let a push one symbol and switch between two source states. Use c(a)=1. Exact reachable rows are e=0 with even z in the initial state and odd z in the other. Formula (6) checks the parity shift. This exercises genuinely infinite periodic sets; it is not a claim that parity is necessary for a coarser certificate of this example.

A negative presentation. Independent push/keep choices on x permit heights 0 and n after x^n. Any input clock has the same H(x^n) for both runs, so one discrepancy is at least n/2. No finite certificate exists for any clock. A proposed zero-clock invariant containing only e=0,1 and z=0 fails at the second push. The unbounded argument proves impossibility; that single checker rejection alone does not. With all states accepting, the language is x*, which has a finite-state implementation. There is no language lower bound here.

Why a plain strip fails. For the bottom pop/keep source and zero clock, the strip |h-H|<=B contains (h,H)=(B+1,2B+1). A pop is enabled and leaves the strip through displacement -B-1. Even a finite union of unrestricted diagonal rays fails: take its smallest displacement and a point with both heights positive, then pop. Yet only (0,0) is reachable. Restricting the common height z is essential for this certificate approach. This failure concerns that invariant format, not every method of proving boundedness.

7. Established ingredients and additional work

Regular forward reachability of pushdown configurations is classical. Schwoon, Model-Checking Pushdown Systems (2002), Section 3.1.2 and Theorem 3.3 (printed page 41; PDF page 51), states correctness of post* saturation; Section 3.1.4 and Theorem 3.5 give an effective implementation. Theorem 3.3 and its stated model were inspected in the primary thesis. This work develops the Esparza, Hansel, Rossmanith and Schwoon algorithms (CAV 2000), with earlier pushdown reachability work by Bouajjani, Esparza and Maler and others. Unary regularity implies eventual periodicity by the elementary finite-state repetition argument given above.

Finite inductive invariants, regular configuration sets, synchronization and VPA determinization are established methods. The additional argument here is the exact diagonal-coordinate reduction with reflected boundaries, its complete finite certificate format for this one-counter subclass, and composition with the stated scaffold resource contract. This is a proved specialization within the Lab’s program, not an established new literature result. The unknown-bound synthesis problem is left open by this note.

The earlier comparisons with residual and bisimulation theory, persistent data structures, pointer-machine simulations, transducer uniformization and lower bounds retain their scope in the foundational contracts. None of those theories is being replaced by a height certificate. The clock is a finite input transducer, not a selector for arbitrary source choices. Immutable cons records provide reuse of a stack tail, not recovery of every past operation. Language equivalence remains weaker than stored-graph equivalence. There is no pumping assertion, so neither repeatability nor recurrence is inferred from periodic reachable heights, and no unrestricted PEG pumping conclusion is drawn.

Primary dependencies:

• Schwoon, 2002, Sections 3.1.2 and 3.1.4.
• Esparza, Hansel, Rossmanith and Schwoon, CAV 2000 record.
• Alur and Madhusudan, corrected author version, imported through the bounded-skew note for visibly pushdown determinization.
• Nowotka and Srba, 2007, for the established height-deterministic setting and clock-convention comparison.
• Reviewed immutable-record compiler.

8. Verification and next question

The executable checker implements the complete finite obligations on supplied certificates, with concrete failed inclusion witnesses. It accepts a JSON instance and also emits reproducible example certificates and a bounded audit in its default mode. The recorded output separates exact certificate decisions from finite checks of the coordinate formulas and periodic inclusion implementation. Those finite checks corroborate the code; the written proofs justify unrestricted soundness and completeness. No pushdown saturation engine, automatic certificate synthesis, VPA determinizer, scaffold generator or proof-assistant development is included.

The next mathematical question is whether an analogous complete, finitely checkable invariant can retain stack contents for a source with several stack symbols. The present height rows cannot test a nontrivial top symbol. The candidate route is to use regular languages of aligned stack contents with bounded unmatched suffixes, then prove both effective closure checks and completeness via a genuine pushdown encoding. A finite abstraction of heights alone would erase exactly the information those guards require.