A quadratic form generalization of rational dinv

Abstract We introduce a quadratic form Q on the space of functions on the gap poset G of the numerical semigroup a, b ⟨ a, b ⟩. We prove combinatorially that when evaluated on the indicator function of an upward closed subset D, this quadratic form precisely recovers the Gorsky–Mazin dinv 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- dinv dinv statistic, which is non-negative. Combining these, we prove the inequality aligned Q (n) 1|G|\, n _ ² aligned Q (n) ≥ 1 | G | ‖ n ‖ ∞ 2 if n 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.