Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Initial Spine Band

Abstract

The initial spine of an avoiding level sequence lies in a controlled band of values.

Theorem 1.1 (Initial spine band).

Lean statement: D5/S3/Combinatorics/LevelSequence/LevelSequenceSpine.initial_spine_band

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

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 an avoiding word, the maximal initial weakly increasing spine has entries bounded below by its first entry and above by the first entry plus its available slack.

References