First Betti numbers of five-generated numerical semigroups
A Lean 4 / Mathlib formalization project for (F) an explicit two-parameter family of minimally five-generated numerical semigroups , m = 2kq+1, whose toric ideal has spanRank exactly 4k+2. Planned scope for (W), a proposed finite-width bound beta1 <= 2w+2 (4 <= w <= 40), not all formalized: the generic fiber-graph infrastructure, both algebraic bridges (only the upper bridge is formalized; the reverse bridge is not), the corrected singleton-counting decomposition beta1 + p = 5 + N, the pair-component antichain lemma and certificate-checker soundness (not yet written). Version 1 targets F; W…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-17-000014
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-17-000014/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-000014/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'