Papers With

← All papers
First page of The e-positivity of $\mathrm{rowDiv}_k(e_μ)$

The e-positivity of $\mathrm{rowDiv}_k(e_μ)$

Per Alexandersson, Lilan Dai

math.CO Oct 19, 2026 · v2
formalization combinatorics algebra
Read PDF arXiv abstract Code
TL;DR
The main e-positivity theorem and the closed-walk coefficient formula are formalized in Lean 4, with a public GitHub repository.
Abstract
We prove that the partition division operator $\mathrm{rowDiv}_k$ preserves e-positivity, resolving a conjecture of Alexandersson and Dai. For $μ\vdash kn$ and $ν\vdash n$, we express the coefficient of $e_ν$ in $\mathrm{rowDiv}_k(e_μ)$ as a normalized sum of positive rational weights over closed walks on a finite directed graph of $k$-restricted partitions. The proof combines the Pieri rule and a root of unity factorization for Macdonald polynomials. As a corollary, we recover the h-positivity of the symmetric functions $A_{n,k}$ of Amdeberhan, Shareshian, and Stanley.
Problem

Alexandersson and Dai conjectured that the partition division operator rowDiv_k, which keeps monomial terms with all parts divisible by k and divides those parts by k, sends each elementary symmetric function e_μ to an e-positive symmetric function.

Approach

For μ ⊢ kn and ν ⊢ n, the coefficient of e_ν in rowDiv_k(e_μ) is expressed as a normalized sum of positive rational weights over closed walks on a finite directed graph of k-restricted partitions. The proof uses the Pieri rule for Macdonald polynomials. It also uses a factorization of Macdonald polynomials when q is specialized to a primitive k-th root of unity, combined with a root-of-unity filter and transfer matrices. The main theorem and the walk formula are formalized in Lean 4.

Results

The conjecture is proved, so rowDiv_k preserves e-positivity. As a corollary, the h-positivity of the symmetric functions A_{n,k} of Amdeberhan, Shareshian, and Stanley is recovered. A Lean 4 formalization is available at github.com/PerAlexandersson/PartitionDivisionLean.