Fel's Conjecture on Syzygies of Numerical Semigroups

TL;DR

This paper proves Fel's conjecture relating syzygy power sums of numerical semigroups to gap power sums and symmetric polynomials, using formalized proof techniques and automated theorem proving.

Contribution

It provides a formal proof of Fel's conjecture on syzygy power sums, connecting algebraic and combinatorial invariants of numerical semigroups.

Findings

Fel's conjecture is proven using exponential generating functions.

Universal identities for symmetric polynomials are derived and verified.

The proof is fully formalized in Lean/Mathlib and generated automatically.

Abstract

Let $S=\langle d_1,\dots,d_m\rangle$ be a numerical semigroup and $k[S]$ its semigroup ring. The Hilbert numerator of $k[S]$ determines normalized alternating syzygy power sums $K_p(S)$ encoding alternating power sums of syzygy degrees. Fel conjectured an explicit formula for $K_p(S)$, for all $p\ge 0$, in terms of the gap power sums $G_r(S)=\sum_{g\notin S} g^r$ and universal symmetric polynomials $T_n$ evaluated at the generator power sums $\sigma_k=\sum_i d_i^k$ (and $\delta_k=(\sigma_k-1)/2^k$). We prove Fel's conjecture via exponential generating functions and coefficient extraction, solating the universal identities for $T_n$ needed for the derivation. The argument is fully formalized in Lean/Mathlib, and was produced automatically by AxiomProver from a natural-language statement of the conjecture.