Skip to main content
Columbus Labs
All research

Research / Enumerative combinatorics

Generalized stack permutations

Algebraic enumeration of the permutations a generalized (r,s)-stack can produce, with the headline theorem formalized in Lean.

Completed · October 2026 · Lean 4.34.1 · CC BY 4.0 / MIT

Read the paper View on GitHub
1278OUTIN3546r = 2s = 2UNBOUNDED HEIGHT

01

The question

A generalized (r,s)-stack inserts each incoming entry into one of its top r positions and removes an entry from one of its top s positions. The stack has unrestricted height.

Which permutations can that machine generate, and, equivalently by inversion, which can it sort? How many of each length are there?

02

Headline theorem

For every fixed pair of positive widths r, s, the counting series of generalized stack permutations is algebraic. For the (3,3)-stack it satisfies a 69-term polynomial equation of degree exactly 12.

Generated outputs and sortable inputs are counted as distinct permutations, related by a proved inversion; the empty permutation is counted once.

Also established

  • A mechanism-based derivation of the known cubic for permutations sortable by a generalized (2,2)-stack.
  • Exact physical-capacity series, minimum-memory statistics, and a Brownian limit for asymptotic capacity.
  • Constructive obstruction families that separate finite and infinite bases, and the capacity threshold between them.

03

Formal verification

  • The algebraicity theorem is formalized end to end for every fixed pair of positive integer widths, at every size including zero. The construction supplies its own decomposition, routing, representation, and uniform-admissibility witnesses.
  • For (3,3), the certificates identify the actual counting series with the specified branch, prove its 69-term polynomial relation, and establish algebraic degree exactly 12, including that no nonzero polynomial of smaller degree annihilates it.
  • Companion certificates cover the (2,2) enumeration, the exact bounded-capacity recurrence, the infinite-basis and container results, and the finite-side basis cardinalities and obstruction-family widths.

Scope. Analytic capacity asymptotics and the complete finite basis grammars keep their separately stated written-proof scope. Finite checks corroborate the implementations; they do not replace all-length proofs.

04

Papers

05

Reproduce and cite

Claim-by-claim scope Lean certificate guide Reproduction guide Release 2026-10-14 
@misc{columbuslabs2026stack,
  author       = {{Columbus Labs}},
  title        = {Generalized stack permutations},
  year         = {2026},
  note         = {Release 2026-10-14},
  howpublished = {\url{https://github.com/ColumbusLabs/generalized-stack-sorting}}
}

The papers are licensed under CC BY 4.0 and the original code and Lean sources under MIT. See the repository for exact license coverage and third-party notices.

More research