Papers, exact algebraic certificates, and reproducible Lean sources from Columbus Labs.
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. This repository studies the distinct permutations generated by that machine and, equivalently by inversion, the permutations it can sort.
The paper titles below open the PDF editions. Each paper also has a formatted Markdown reading copy and LaTeX source.
- Algebraic enumeration of generalized stack permutations. Algebraicity for every fixed pair of positive widths, with a degree-12 equation for
(3,3). Reading copy · LaTeX source - A direct enumeration of permutations sortable by a generalized (2,2)-stack. A mechanism-based derivation of the known cubic. Reading copy · LaTeX source
- Physical capacity in a generalized stack: exact series and a Brownian limit. Exact capacity series, minimum-memory statistics, and asymptotic capacity. Reading copy · LaTeX source
- Finite and infinite bases for generalized stacks. Constructive obstruction families and the capacity threshold. Reading copy · LaTeX source
The headline algebraicity theorem is formalized end to end for every fixed pair of positive integer widths r,s, at every size including zero. The construction supplies its decomposition, routing, representation and uniform-admissibility witnesses. It counts distinct generated outputs and sortable inputs, related by proved inversion; the empty permutation is counted once.
The (3,3) certificates additionally identify the actual counting series with the specified scalar branch, prove its 69-term polynomial relation, and establish algebraic degree exactly 12 for both counting series. This includes the nonexistence of a nonzero annihilating polynomial of smaller degree.
The companion certificates cover the (2,2) enumeration, the exact bounded-capacity recurrence, the infinite-basis and container results, and the added finite-side basis cardinalities and exact obstruction-family widths. See the claim-by-claim scope and certificate guide for precise hypotheses and reproduction instructions. Analytic capacity asymptotics and the complete finite basis grammars retain their separately stated written-proof scope. Finite checks corroborate implementations; they do not replace all-length proofs.
Start with REPRODUCE.md. It separates source-integrity checks, bounded Python tests, exact-algebra verification, PDF builds, and source-only Lean compilation. No compiler binaries or compiled project objects are distributed.
papers/: manuscripts, bibliography, and displayed equation datasrc/andtests/: executable finite models and regression testsdocs/andresearch/: supporting mathematical arguments and exact algebraic dataformal/: Lean sources, pinned toolchains, dependency manifests, and replay scriptsMANIFEST.json: exact release-file hashes
Author and contact: Columbus Labs · info@columbus-labs.com
The papers, original figures, and original expository text are available under CC BY 4.0. Original software and Lean source code are available under the MIT License. See license coverage and third-party notices. Attribution is required under the applicable license; commercial reuse and modification are permitted.