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.

Disclosure

“ch paper is a narrative designed to communicate ideas to people, whereas a Lean file is written to satisfy a proof-checking kernel. At first glance, therefore, the formal proofs do not resemble the narrative presented here. Declaration of generative AI and AI-assisted technologies in the manuscript preparation process As described in the preceding appendix, AxiomProver was used to produce and formally verify, in Lean, the proofs of Theorem 1.3, Corollary 1.4, a”

PDF page 12

Classification

Proof ideas or individual proof-step assistance

Multiplier

8

Verified

2026-08-23T19:18:39.734632Z

Structural counts