On a conjecture of Han and Xiong for fractional Gaussian binomial coefficients

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.