Catalan Enumeration of Level Sequences

Abstract

The level sequences avoiding 101 and 102 are counted by the Catalan numbers.

Theorem 1.1 (The Catalan enumeration).

Lean statement: D5/S3/Combinatorics/LevelSequence/LevelSequenceCatalan.result

Proof. Machine-checked in Lean as D5/S3/Combinatorics/LevelSequence/LevelSequenceCatalan.result (✓ std3). ∎

Resolves. Problems/mansour-level-sequences-101-102-catalan (proved) by D5/S3/Combinatorics/LevelSequence/LevelSequenceCatalan.result.

Source. Repository-derived.

Acknowledgement. Toufik Mansour (2026). Wilf Classes for Level Sequences Avoiding Patterns of Length Three. DOI: 10.3390/math14111983. URL: https://www.mdpi.com/2227-7390/14/11/1983.

Commentary.

For every positive n, the number of level sequences of length n avoiding 101 and 102 equals the Catalan number at index n.