{"id":"palomar/PALOMAR-2026-10-17-000014","url":"https://github.com/benkeene/five-generator-betti/tree/8c57c1eaf991f5dbb1001fbc5f18835388787453","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-17-000014-v2.json","repo":"https://github.com/benkeene/five-generator-betti","tags":["math.AC","math.CO","msc:13D02","msc:20M14","msc:13F65","msc:05E40","numerical-semigroups","commutative-algebra","lean","formalization"],"score":0,"title":"First Betti numbers of five-generated numerical semigroups","trust":"high","domain":"math.AC","source":"palomar","authors":["Ben Keene"],"reviews":0,"subject":"math.AC","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-23","reactions":{},"formalized":true}