On a conjecture of Han and Xiong for fractional Gaussian binomial coefficients
Ken Ono
math.CO
Jul 31, 2026 · v1
TL;DR
Support-dominance theorem for fractional Gaussian binomial coefficients was autonomously produced and verified in Lean by the AxiomProver AI system.
Abstract
Han and Xiong recently extended the Gaussian binomial coefficient $\genfrac{[}{]}{0pt}{}{r+k}{k}_{q}$ to positive rational $r$ and conjectured that its integer trace, the integer-exponent part of the resulting power series, is coefficientwise largest at $r=1/2$. We prove a support-dominance theorem comparing rational parameters under an explicit divisibility condition. It settles the conjecture for every $r\geq 1/2$ and reduces the full conjecture to the unit fractions $r=\frac{1}{2m}$, only finitely many of which are nontrivial for each fixed $k$. A computer computation then verifies the conjecture for every positive rational $r$ and every $k\leq 200$. The theoretical results were autonomously produced and verified in Lean by AxiomProver.
Problem
Han and Xiong extended Gaussian binomial coefficients to positive rational parameters r and conjectured that the integer trace of the resulting power series is coefficientwise largest at r=1/2.
Approach
A support-dominance theorem compares rational parameters u and r under an explicit divisibility condition, using an exact trace formula and a shift-dominance lemma to obtain coefficientwise dominance summand by summand. The theoretical results were autonomously produced and verified in Lean by AxiomProver. A computer computation supplements the proof for finitely many remaining cases.
Results
The conjecture is settled for every r>=1/2 and reduced to unit fractions r=1/(2m), only finitely many nontrivial for each fixed k. The computation verifies the conjecture for every positive rational r and every k<=200.
