Boolean and distributive intervals in the two Bruhat orders on the symmetric group
Abstract
Two exercises of Stanley, reprinted as Problems 21 and 22 of Worley's notebook of open problems, ask which intervals of the symmetric group Sₙ are boolean algebras in the strong Bruhat order, which are distributive lattices in the weak order, and how many there are of each. We settle the enumeration in the strong Bruhat order for n ≤ 7: the number of boolean intervals is 1, 3, 18, 174, 2403, 44190, 1033578 for n=1,…,7. These values appear not to be recorded anywhere; the most recent paper on the subject asks precisely for the proportion of Bruhat intervals that are boolean. For the weak order we correct the value printed at n=2 in the notebook and in the textbook: the weak order on S₂ has three intervals and all three are distributive lattices, so the value is 3 and not 2. We then re-derive the published counts 1, 3, 16, 124, 1262, 15898, 238572 for n ≤ 7 directly from the definitions, without using the known characterization, and we verify that characterization — an interval [u,v] of the weak order is a distributive lattice if and only if u⁻¹v avoids the pattern 321 — at every one of the 1899, 31711 and 672697 intervals of S₅, S₆ and S₇. Every theorem below, and each exhaustive search behind it, is machine-checked in Lean 4.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-08-30 15:34 UTC
File fingerprint
a86ca9b6252c9634408f0cc1460d7ad8fe9e043646e4d117670eed0c40385b26
Claim ledger
Stated results
T1candidate2026-08-23
Problem 21: the number of boolean intervals of the strong Bruhat order on Sₙ is 1, 3, 18, 174, 2403 for n <= 5
T2known2026-08-22
Two published theorems of Tenner reproduced as cross-checks on the boolean test
T3known data2026-08-22
Problem 22: the number of distributive intervals of the weak order on Sₙ is 1, 3, 16, 124 for n <= 4 – and the printed value 2 at n = 2 is wrong
T4known2026-08-22
Stembridge's characterization verified: a weak-order interval [u,v] of S₄ is distributive exactly when u⁻¹v is 321-avoiding
T5routine2026-08-22
Negative controls: not every interval is boolean/distributive, and interval size alone does not characterize boolean-ness
T6candidate2026-08-23
Problem 21 at n = 8: 29757420 boolean intervals (external only; n = 6, 7 are now theorems T8/T9)
This ledger entry is reported in prose and is not bound to a Lean theorem.T7known data2026-08-22
Problem 22 at n = 5 and n = 6: 1262 and 15898 distributive intervals
This ledger entry is reported in prose and is not bound to a Lean theorem.T8candidate2026-08-23
Problem 21 at n = 6: the strong Bruhat order on S₆ has 44190 boolean intervals
T9candidate2026-08-23
Problem 21 at n = 7: the strong Bruhat order on S₇ has 1 033 578 boolean intervals
T10routine2026-08-23
The tabulated evaluation engine is proved equal to the definition, kernel-clean
T11routine2026-08-23
Negative controls at n = 6 and n = 7
T12routine2026-08-23
Gate: the tabulated engine re-derives n ≤ 5 through a route sharing no code with the original
T13known data2026-08-23
Problem 22 at n = 5: the weak order on S₅ has 1262 distributive intervals
T14known data2026-08-23
Problem 22 at n = 6: the weak order on S₆ has 15898 distributive intervals
T15known data2026-08-23
Problem 22 at n = 7: the weak order on S₇ has 238572 distributive intervals
T16routine2026-08-23
The tabulated weak-order engine is proved equal to the definition, kernel-clean
T17routine2026-08-23
Gate: the tabulated weak-order engine re-derives n <= 4 through a route sharing no code with the original
T18routine2026-08-23
Negative controls for Problem 22 at n = 5, 6 and 7
T19known2026-08-23
Stembridge's characterization verified on S₅, S₆ and S₇: a weak-order interval [u,v] is a distributive lattice iff u⁻¹v is 321-avoiding
T20routine2026-08-23
The characterization check means what it says: one finite Bool implies the statement about WeakLE and IsDistributiveOn, kernel-clean
T21known data2026-08-23
The Stembridge side computed alone reproduces A190291 at n <= 7, and the interval counts are A007767
T22routine2026-08-23
Negative controls for the characterization at n = 5, 6, 7, including the excluded non-comparable pair and a refuted neighbouring pattern
Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Two problems from Dale R. Worley's open-problem notebook (arXiv:2509.25446 v3), both quoted there from Stanley's *Enumerative Combinatorics* vol. 1, 2nd ed., Ch. 3, and both rated [5–].
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7