Add Fel's Conjecture project; port to v4.30.0-rc2 Mathlib

LeanPool.lean

@@ -1 +1,3 @@
 import LeanPool.Basic
+import LeanPool.FelConjecture
+import LeanPool.FelConjecture.Solution

LeanPool/FelConjecture.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2026 Evan Chen, Kenny Lau, Ken Ono, Jujian Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Evan Chen, Kenny Lau, Ken Ono, Jujian Zhang
+-/
+
+import LeanPool.FelConjecture.Solution
+
+/-!
+# 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
+-/
+
+/-!
+## 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](https://axiommath.ai). Upstream contains no
+`sorry`s in the solution file. Ported from Lean v4.26.0 to Lean Pool's
+v4.30.0-rc2.
+-/