NumericalSemigroups: Huang's quadratic form, its positivity, and its n-generator kernel windows
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|…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-17-000016
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-17-000016/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-17-000016/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'