Documentation

LeanPool.FelConjecture

Fel's Conjecture on Syzygies of Numerical Semigroups #

Source: arxiv:2602.03716 Authors: Evan Chen, Kenny Lau, Ken Ono, Jujian Zhang Status: verified Main declarations: fels_conjecture Tags: number-theory, combinatorics, polynomials MSC: 20M14, 13D02

Mathematical overview #

A numerical semigroup S ⊆ ℕ is an additive submonoid containing 0 with finite complement (the gaps Δ = ℕ \ S). Given generators {d₁,…,d_m} with gcd = 1, the project defines gap power sums, the gap polynomial, the Hilbert series and its numerator Q_S, alternating power sums C_n(S), and the invariants K_p(S) along with the symbols T_n(σ), T_n(δ) from generating-series factorisations.

The main result, fels_conjecture, expresses each K_p(S) as a finite combination of gap power sums and the T symbols.

Provenance #

Imported from https://github.com/AxiomMath/fel-polynomial; initial code generated by Axiom Math. Upstream contains no sorrys in the solution file. Ported from Lean v4.26.0 to Lean Pool's v4.30.0-rc2.