A quadratic form generalization of rational dinv

TL;DR

This paper introduces a quadratic form on functions over the gap poset of a numerical semigroup, connecting it to the dinv statistic and proving positivity properties, with formalization in Lean/Mathlib.

Contribution

It generalizes the rational dinv statistic via a quadratic form and establishes new inequalities and a formal proof in Lean/Mathlib.

Findings

Quadratic form $Q$ recovers the dinv statistic on upward closed subsets.

The associated bilinear form defines a new cross-dinv statistic that is nonnegative.

Proves a positive definiteness inequality for $Q$ on decreasing functions.

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.