{"id":"palomar/PALOMAR-2026-10-17-000016","url":"https://github.com/Flaman55/NumericalSemigroups/tree/a872b68c6a0d0f09fba702347fdc75b3b5ec8491","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-17-000016-v1.json","repo":"https://github.com/Flaman55/NumericalSemigroups","tags":["math.CO","math.NT","msc:20M14","msc:11D07","numerical-semigroups","quadratic-forms","lean","combinatorics"],"score":0,"title":"NumericalSemigroups: Huang's quadratic form, its positivity, and its n-generator kernel windows","trust":"high","domain":"math.CO","source":"palomar","authors":["Artur Flamandzki"],"reviews":0,"subject":"math.CO","summary":"Lean 4 / Mathlib formalization around the quadratic form Q(n) = sum_{i,j in G} K(g(j) - g(i)) n_i n_j of Y. Huang (arXiv:2604.13238) on the gap diagram G of the numerical semigroup , in two parts. Part A (Huang's results, two generators): the symmetric bilinear form B of Q satisfies B(1_D, 1_E) = dinv(D, E) for subdiagrams D, E (Huang's Theorem 1.2, formalized by AxiomProver and included in `Dinv/AxiomProver.lean`); from it this work proves Q(1_D) = dinv(D) and Q(1_D) > 0 for nonempty D (Theorem 1.1), B >= 0 on the cone of nonnegative decreasing functions, and the bound Q(n) >= n_i^2 / |G|…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-17","reactions":{},"formalized":true,"formalizes":[{"title":"A quadratic form generalization of rational dinv","identifier":"arXiv:2604.13238","relationship":"formalizes"},{"title":"A Linear Algorithm for Huang's Quadratic Form on Numerical Semigroups and Density Asymptotics","identifier":"https://zenodo.org/records/20261427","relationship":"formalizes"}]}