Skip to main content
Columbus Labs
All research

Research / Dynamical algebraic combinatorics

Sharp exceptional density for interval-closed rowmotion

The exact leading rate at which rowmotion on interval-closed sets misses its generic period, proved for every fixed width and verified in Lean.

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

Read the paper View on GitHub
[3] × [6]INTERVAL-CLOSEDPERIOD n + m + 1

01

The question

Rowmotion is a map built from toggles that acts on subsets of a partially ordered set. On interval-closed subsets of the rectangle [m] × [n], the generic least period is n + m + 1.

Lafrenière, Lewis, McNicholas, Striker, and Welch conjectured that, for fixed width, almost every subset has that period as n grows. How quickly do the exceptions vanish?

02

Main theorem

For every fixed integer m ≥ 2, the proportion of interval-closed subsets of [m] × [n] whose least rowmotion period differs from n + m + 1 isEm(n) / Am(n) = m(m − 1)/n + Om(n−2)

This determines the leading exceptional-density coefficient and proves the fixed-width density-one conjecture. The constants and onset may depend on m.

Also established

  • Density one for every fixed positive width, including width one.
  • Exceptional fraction at most min(1, 73m³/n) for m > 0 and n ≥ 4m² + 11m − 1, hence density one when m = o(n^(1/3)).
  • At width three, limiting exceptional-state shares of 2/5 and 3/5 for periods 2n + 10 and 3n + 14, with vanishing remaining share.
  • The exact row-nonempty Narayana enumeration, with credit to prior work.
  • A general coprime-cycle least-period theorem, plus explicit width-four chamber families and an all-width two-block family with exact least periods.

03

Formal verification

  • The Lean endpoint RowmotionSharpAllWidth.actualRowmotion_sharp_all_width takes only a natural number m and the hypothesis m ≥ 2.
  • The proof closure contains 225 mathematical modules. The recorded verification audited 9,278 project declarations and replayed the complete imported environment into a fresh instance of the pinned Lean kernel.
  • The only axiom dependencies are propext, Classical.choice, and Quot.sound. The companion results have their own complete Lean sources.

Scope. The PDF presents the main fixed-width theorem; the companion results are documented in a separate guide with their exact hypotheses. No complete classification of finite orbits is claimed.

04

Paper

05

Reproduce and cite

Companion results guide Lean companion Theorem-to-source map Reproduction guide Release 2026-10-14 
@article{columbuslabs2026rowmotion,
  author = {{Columbus Labs}},
  title  = {Sharp exceptional density for rowmotion on interval-closed sets of a rectangle},
  year   = {2026},
  url    = {https://github.com/ColumbusLabs/interval-closed-rowmotion}
}

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