Sharp parity-sensitive Gauss coefficient upper bound
Abstract
Sharp parity-sensitive Gauss coefficient upper bound.
Theorem 1.1 (Sharp leading upper bound).
Lean statement: D5/S3/Combinatorics/TwoColorPartition/AndrewsElBachraouiFiveGauss.gauss_coefficient_upper
Proof. Machine-checked in Lean as D5/S3/Combinatorics/TwoColorPartition/AndrewsElBachraouiFiveGauss.gauss_coefficient_upper (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. George E. Andrews, Mohamed El Bachraoui (2025). Certain positive q-series and inequalities for two-color partitions. DOI: 10.48550/arXiv.2507.09276. URL: https://arxiv.org/abs/2507.09276v1.
Commentary.
For every natural n, the real coefficient of productTrunc 2 n is at most pi over four times n, plus five quarters times the square root of twice n plus one half, plus pi over sixteen and three eighths. The proof keeps the parity-compatible triangular rows, bounds their square-root sums by a quarter-circle integral, and applies the existing exact Gauss coefficient count. This upper bound is sufficient for the full eventual result.