Papers With

← All papers
First page of Counterexamples to the Reiner-Shimozono conjecture and the failure of Schubert filtrations

Counterexamples to the Reiner-Shimozono conjecture and the failure of Schubert filtrations

Reuven Hodges

math.RT Sep 23, 2026 · v2 math.CO
formalization mathlib combinatorics algebra
Read PDF arXiv abstract
TL;DR
The main counterexample theorem (Theorem 1.1) was formalized in Lean 4 with Mathlib, with the formalization produced using an AI model.
Abstract
We disprove the Reiner–Shimozono conjecture that products of key polynomials have nonnegative expansions in Demazure atoms. By relaxing the defining relations of Demazure modules, we obtain an exact coefficient-extraction formula that yields an explicit infinite family of counterexamples, including negative coefficients in twenty-eight variables. These examples answer van der Kallen's long-standing open question on relative Schubert filtrations negatively, already for tensor products of two dual Joseph modules. For individual atom coefficients, we give a sufficient criterion for positivity that is checkable in polynomial time in the binary input length, uniformly in rank. For each fixed rank $n\ge4$, this criterion recognizes a nonvanishing proportion of the positive atom coefficients as the bound on the composition entries tends to infinity.
Problem

The Reiner–Shimozono conjecture predicts that products of key polynomials expand nonnegatively in the Demazure atom basis. A related long-standing open question of van der Kallen asks whether tensor products of modules with excellent filtrations admit relative Schubert filtrations.

Approach

Demazure modules are replaced by larger 'relaxed Demazure modules' whose simpler characters allow exact extraction of individual atom coefficients. Fu–Lascoux key/atom duality turns an atom coefficient into a Laurent coefficient. That coefficient is then reduced via Hall-polynomial extraction to a finite signed count. A quiver-multiplicity interpretation gives a positive lattice-point formula under explicit hypotheses. Theorem 1.1 was formalized in Lean 4 using Mathlib.

Results

An explicit infinite family of counterexamples is constructed, including negative coefficients in 28 variables. These counterexamples also answer van der Kallen's question negatively. A polynomial-time sufficient positivity criterion is given, and for each fixed rank n≥4 it detects a nonvanishing proportion of positive atom coefficients.