Papers With

← All papers
First page of The Schur positivity of Lucas binomial differences

The Schur positivity of Lucas binomial differences

Lilan Dai, Dun Qiu, Weichen Wang, Minhao Zhang

math.CO Oct 26, 2026 · v1
formalization combinatorics algebra
Read PDF arXiv abstract Code
TL;DR
The main theorems on Schur and e-positivity of Lucas binomial and multinomial differences are formalized in Lean 4, with a public GitHub repository.
Abstract
For positive integers $a\le b\le c\le d$ with $ad=bc$, we prove that the Lucas binomial coefficients satisfy $(-1)^{a+1}(L_{b,c}[X]-L_{a,d}[X])\in\mathbb{N}[e_1[X],e_2[X],h_2[X]]$, resolving Bergeron's conjecture on Schur positivity in two variables. We also prove the same positivity for $L_{u,v}[X]-e_1[X]^{uv-rs}L_{r,s}[X]$ when $rs<uv$. Using Lucas atoms, we establish $e$-positivity for degree-adjusted Lucas multinomial differences under dominance order.
Problem

Bergeron conjectured that for positive integers a≤b≤c≤d with ad=bc, the difference of Lucas binomial coefficients L_{b,c}[q+t]−L_{a,d}[q+t] is Schur positive up to a global sign. This is a Lucas analogue of a question on differences of Gaussian binomial coefficients.

Approach

Lucas binomial coefficients are treated as polynomials in e_1 and e_2 within symmetric functions. Coefficient formulas are derived for the differences in the basis e_1^δ h_2^{M−j} e_2^j, using the specialization to Gaussian polynomials and generating-function estimates based on the factorization of words into Lyndon words. Dominance-order chains of partitions and Lucas atoms are used to handle the multinomial case. Theorems 1.2, 1.4 and 1.5 are formalized in Lean 4.

Results

(−1)^{a+1}(L_{b,c}−L_{a,d}) lies in N[e_1,e_2,h_2], which resolves Bergeron's conjecture. Analogous positivity holds for L_{u,v}−e_1^{uv−rs}L_{r,s} when rs<uv, and degree-adjusted Lucas multinomial differences are e-positive under dominance order.