Finite-Ones Compactness and Resource-Existence Decidability for Epsilon-Free Deterministic Pushdown Automata

The paper follows our binary deterministic pushdown resource-hierarchy work and addresses a different question: whether any equivalent epsilon-free recognizer exists within prescribed numbers of states and stack symbols. This is not an ordinary finite search, because a transition may push an arbitrarily long word even when the two resource counts are fixed. The paper proves that a finite-ones completion property of the target language yields a finite-horizon bound on the physical stack needed by every correct competitor. A deletion-only compactness argument then converts success at all finite horizons into one globally correct finite transition table. Combined with deterministic pushdown equivalence, this gives a terminating yes-or-no procedure and finite, mechanically checkable word certificates for negative resource instances. The method extends to effectively zero-drain-calibrated languages without imposing a fixed push-length bound. Its main novelty is a language-driven compactness mechanism that resolves a resource-existence problem over an apparently infinite space of epsilon-free machines, distinct from equivalence testing for two machines already given. It does not claim the same decision result for epsilon-enabled competitors.