Fel's Conjecture on Syzygies of Numerical Semigroups

Technical Summary: Fel's Conjecture on Syzygies of Numerical Semigroups

Problem Statement
The paper addresses a conjecture proposed by Leonid Fel regarding the structure of syzygies in the semigroup ring $k[S]$ of a numerical semigroup $S = \langle d_1, \dots, d_m \rangle$. The Hilbert series of $k[S]$ is given by $HS(z) = Q_S(z) / \prod_{i=1}^m (1-z^{d_i})$, where $Q_S(z)$ is the Hilbert numerator. This numerator is an alternating sum of monomials $z^{C_{i,j}}$, where the exponents correspond to the degrees of syzygies.

Fel introduced normalized alternating syzygy power sums, denoted $K_p(S)$, which encode alternating power sums of these syzygy degrees. Specifically, $K_p(S)$ relates to the alternating power sums $C_{m+p}(S)$ via the formula:
$$C_{m+p}(S) = (-1)^m \pi_m \frac{(m+p)!}{p!} K_p(S)$$
where $\pi_m = \prod d_i$.

Fel conjectured an explicit closed formula for $K_p(S)$ for all $p \ge 0$. This formula expresses $K_p(S)$ as a linear combination of:

1. Gap power sums: $G_r(S) = \sum_{g \notin S} g^r$, where the sum is over the gap set $\Delta = \mathbb{Z}_{\ge 0} \setminus S$.
2. Universal symmetric polynomials: $T_n(\sigma)$ and $T_n(\delta)$, evaluated at the generator power sums $\sigma_k = \sum d_i^k$ and the shifted values $\delta_k = (\sigma_k - 1)/2^k$.

The conjecture states:
$$K_p(S) = \sum_{r=0}^p \binom{p}{r} T_{p-r}(\sigma) G_r(S) + \frac{2^{p+1}}{p+1} T_{p+1}(\delta)$$

Methodology
The authors prove the conjecture using a direct formal power series argument centered on exponential generating functions (EGF). The core strategy involves translating the combinatorial definitions of syzygy degrees and gap sets into the language of EGFs to isolate universal identities.

1. Generating Function Translation:

   • The authors define the gap polynomial $\Phi_S(z) = \sum_{g \in \Delta} z^g$. They show that the EGF for the gap power sums $G_n(S)$ is simply $\Phi_S(e^t)$.
   • They relate the Hilbert numerator $Q_S(z)$ and the denominator $P_S(z) = \prod (1-z^{d_i})$ to the EGFs of the syzygy degrees.
   • Crucially, they utilize the definition of the universal symmetric polynomials $T_n$ via their own EGFs, $A(t)$ and $B(t)$, where $A(t) = \prod \frac{e^{x_i t}-1}{x_i t}$ and $B(t) = \frac{t}{e^t-1}A(t)$.

2. Algebraic Manipulation:

   • By substituting $z = e^t$ into the fundamental identity relating the Hilbert series, the gap polynomial, and the denominator, the authors derive an identity in the ring of formal power series:
     $$1 - Q_S(e^t) = 1 + (-1)^m \pi_m \left( t^{m-1} B(t) + t^m A(t) \Phi_S(e^t) \right)$$
   • They extract the coefficient of $t^{m+p}$ from both sides of this equation.
   • On the left side, the coefficient corresponds to the normalized syzygy sum $C_{m+p}(S)$.
   • On the right side, the coefficient extraction involves the Cauchy product of the series for $A(t)$, $B(t)$, and $\Phi_S(e^t)$. This operation naturally yields the binomial convolution of the universal polynomials $T_n$ with the gap sums $G_r$, and the specific term involving $T_{p+1}(\delta)$.

3. Formalization:
   The entire argument was formalized in the Lean theorem prover using the Mathlib library. The proof was generated automatically by AxiomProver, an AI tool, starting from a natural-language statement of the conjecture.

Key Contributions and Results

• Proof of Conjecture 1.6: The paper provides a rigorous proof that Fel's explicit formula for $K_p(S)$ holds for all $p \ge 0$.
• Derivation of Universal Identities: The proof isolates and utilizes specific identities for the universal symmetric polynomials $T_n$, demonstrating how they arise naturally from the interplay between the Hilbert series and the gap set.
• Automated Theorem Proving Case Study: The work serves as a demonstration of AxiomProver's capability to handle non-trivial problems in commutative algebra and additive number theory. The authors note that the proof was produced automatically from the natural-language conjecture, with the authors subsequently refining the exposition for a human mathematical audience.

Significance and Claims
The paper claims to resolve the original "birthplace" of the universal symmetric polynomials $T_n$, which were previously studied in the context of restricted partitions, zig-zag numbers, and Ramanujan's $q$-series (as noted in the introduction). By proving Fel's conjecture, the authors unify these disparate appearances of $T_n$ under the framework of numerical semigroup syzygies.

The authors explicitly frame the work as a "case study and test case" for automated theorem proving. They do not claim to discover new applications for the polynomials beyond the context of the conjecture itself, nor do they propose future experimental directions. The primary significance lies in the successful verification of a complex combinatorial identity and the demonstration of AI-assisted formalization in mainstream mathematics. The paper emphasizes that the mathematical derivation is self-contained and independent of the Lean code, though the code serves as the verified foundation.