A quadratic form generalization of rational dinv
Yifeng Huang
math.CO
Apr 14, 2026 · v1
TL;DR
Main theorem autoformalized in Lean/Mathlib by AxiomProver.
Abstract
We introduce a quadratic form $Q$ on the space of functions on the gap poset $G$ of the numerical semigroup $\langle a,b\rangle$. We prove combinatorially that when evaluated on the indicator function of an upward closed subset $D$, this quadratic form precisely recovers the Gorsky--Mazin $\mathtt{dinv}$ statistic of $D$, viewed as a Young subdiagram of $G$. Furthermore, we prove Theorem~1.2 that when evaluated on a pair of subdiagrams of $G$, the symmetric bilinear form associated with $Q$ is equal to a novel cross-$\mathtt{dinv}$ statistic, which is nonnegative. Combining these, we prove the inequality \[ Q(\mathbf{n})\geq \dfrac{1}{|G|}\,\|\mathbf{n}\|_\infty^2\] if $\mathbf{n}$ is a real-valued decreasing function on $G$, showing an effective positive definiteness of $Q$ on the corresponding cone. Theorem~1.2, the main engine of the paper, was autoformalized in Lean/Mathlib by AxiomProver.
Problem
The Gorsky-Mazin dinv statistic for rational Catalan combinatorics lacks a natural algebraic characterization in terms of quadratic forms, and effective positive-definiteness bounds for such forms on the gap poset of numerical semigroups are not known.
Approach
The authors introduce a quadratic form Q on functions on the gap poset G of the numerical semigroup <a,b>. They prove combinatorially that Q evaluated on the indicator function of an upward closed subset D recovers the Gorsky-Mazin dinv statistic. They also define a cross-dinv statistic via the associated symmetric bilinear form and show it equals the bilinear form on pairs of subdiagrams. They formalize the results in Lean 4.
Results
The quadratic form Q recovers dinv exactly, the cross-dinv statistic is shown to be nonnegative, and the inequality Q(n) >= (1/|G|) * ||n||_infinity^2 is proved for real-valued decreasing functions on G, establishing effective positive definiteness on the corresponding cone.
