Record compositions of alternating permutations and noncommutative symmetric functions
Evan Chen, Ken Ono, Michal Mogielnicki
math.CO
Jul 14, 2026 · v1
math.RT
TL;DR
AxiomProver autonomously formalized and verified the paper's three main combinatorial theorems in Lean 4.31.0.
Abstract
Amdeberhan, Shareshian, and Stanley recently proved that a function $\varphi$ arising in the theory of partition Eisenstein series counts the alternating permutations of $\{1,\dots,2n\}$ with a given `record' partition, and they asked whether there is a similar theory for record compositions, suggesting a role for noncommutative symmetric functions. Here we solve their open problem by showing that the number of alternating permutations of $\{1,\dots,2n\}$ with record composition $(α_1,\dots,α_\ell)$ is \[ \prod_{j=1}^{\ell}\binom{2s_j-1}{2α_j-1}E_{2α_j-1}, \] where $s_j=α_1+\dots+α_j$, $E_k$ is an Euler number, and the record composition of $w=a_1a_2\dots a_{2n}$ (so $a_1>a_2<a_3>\dotsb$) lists the factor lengths obtained by cutting $a_1a_3\dots a_{2n-1}$ before each left-to-right maximum other than the first. These numbers are the coefficients of a natural lift of the degree-$n$ sprout symmetric function with seed $\sec(\sqrt{t}\,)$ to noncommutative symmetric functions, expanded in products of noncommutative power sums of the first kind. An analogous refinement holds for every sprout sequence whose seed is given by the exponential formula. AxiomProver autonomously produced and verified the results in this paper in Lean.
Problem
Amdeberhan, Shareshian, and Stanley asked whether the partition-Eisenstein counting function has an analogue for record compositions of alternating permutations, suggesting a role for noncommutative symmetric functions.
Approach
A bijection between alternating permutations with a given record composition and ordered block data is constructed, splitting the count into block choice and per-block decoration. The result is recast multiplicatively to match a canonical lift of a sprout symmetric function to noncommutative symmetric functions (NSym), expanded in noncommutative power sums. A general refinement is proven for sprout sequences with exponential-formula seeds. The AxiomProver system autonomously generated proofs and formalized/verified the three main theorems in Lean 4.31.0 from a task specification.
Results
The number of alternating permutations of {1,...,2n} with record composition (α₁,...,α_ℓ) equals ∏ binom(2s_j-1, 2α_j-1) E_{2α_j-1}, matching a noncommutative lift's coefficients. Counts were confirmed by exhaustive enumeration and the row sums equal Euler numbers E_{2n}.
| α | N(α) |
|---|
| (4) | 272 |
| (3,1) | 112 |
| (1,3) | 336 |
| (2,2) | 140 |
| (1,1,1,1) | 105 |
N(α) for n=4 compositions (partial)