A quadratic form generalization of rational dinv

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.