The genus bound for numerical semigroups generated in degrees ≤ D

For a numerical semigroup S = ⟨A⟩ ⊆ ℕ with finitely many gaps, generated by elements ≤ D, the genus g (number of gaps) satisfies 2g ≤ (κ − 1)(D − 1) for every κ > 0 in S (the Apéry-set argument), hence 2g ≤ (D − 1)(D − 2), with equality only for ⟨D − 1, D⟩.

Main results

• P3a.genus_pair, P3a.conductor_pair: ⟨m, m + 1⟩ has m(m − 1)/2 gaps and conductor m(m − 1) (the Frobenius number from Mathlib's frobeniusNumber_pair).
• P3a.genus_le: 2g ≤ (κ − 1)(D − 1).
• P3a.genus_le_D: 2g ≤ (D − 1)(D − 2).
• P3a.eq_pair_of_genus_eq: equality forces S = ⟨D − 1, D⟩.

References

• C. Marín, The order generated by a column of the SU(n)_k S-matrix is locally a numerical semigroup ring (Part I), Zenodo (2026), doi:10.5281/zenodo.22848529.

def P3a.gaps (A : Set ℕ) : Set ℕ

The gaps of the additive submonoid of ℕ generated by A.

Equations

• P3a.gaps A = {x : ℕ | x ∉ AddSubmonoid.closure A}

noncomputable def P3a.genus (A : Set ℕ) : ℕ

The genus: number of gaps (Set.ncard, 0 if infinite; every use below assumes finite).

Equations

• P3a.genus A = (P3a.gaps A).ncard

The semigroup ⟨m, m+1⟩

theorem P3a.mem_pair_iff {m : ℕ} (hm : 0 < m) (x : ℕ) : x ∈ AddSubmonoid.closure {m, m + 1} ↔ x % m ≤ x / m

Membership in ⟨m, m+1⟩: x % m ≤ x / m.

theorem P3a.filter_lt_range (m q : ℕ) : {r ∈ Finset.range m | q < r} = Finset.Ioo q m

theorem P3a.card_pairs_lt (m : ℕ) : {p ∈ Finset.range m ×ˢ Finset.range m | p.1 < p.2}.card * 2 = m * (m - 1)

#{(q,r) : q < r < m} * 2 = m(m−1).

theorem P3a.gaps_pair_eq {m : ℕ} (hm : 0 < m) : gaps {m, m + 1} = ↑({x ∈ Finset.range (m * m) | x / m < x % m})

The gaps of ⟨m, m+1⟩ as a finset.

theorem P3a.genus_pair {m : ℕ} (hm : 0 < m) : genus {m, m + 1} * 2 = m * (m - 1)

Genus of ⟨m, m+1⟩: 2·g = m(m−1), i.e. g(⟨n−1,n⟩) = (n−1)(n−2)/2.

theorem P3a.conductor_pair {m : ℕ} (hm : 2 ≤ m) : m * (m - 1) - 1 ∉ AddSubmonoid.closure {m, m + 1} ∧ ∀ (x : ℕ), m * (m - 1) ≤ x → x ∈ AddSubmonoid.closure {m, m + 1}

Conductor of ⟨m, m+1⟩ (m ≥ 2): every x ≥ m(m−1) is in the semigroup and m(m−1) − 1 (the Frobenius number m(m+1) − m − (m+1), Mathlib) is not.

The general bound (Apéry elements of multiplicity κ, generators in degrees ≤ D)

def P3a.L (A : Set ℕ) : ℕ → Set ℕ

L t: sums of at most t elements of A.

Equations

• P3a.L A 0 = {0}
• P3a.L A t.succ = P3a.L A t ∪ {z : ℕ | ∃ y ∈ P3a.L A t, ∃ a ∈ A, z = y + a}

theorem P3a.zero_mem_L (A : Set ℕ) (t : ℕ) : 0 ∈ L A t

theorem P3a.L_sub_closure (A : Set ℕ) (t : ℕ) : L A t ⊆ ↑(AddSubmonoid.closure A)

theorem P3a.L_le (A : Set ℕ) {D : ℕ} (hA : ∀ a ∈ A, a ≤ D) (t y : ℕ) : y ∈ L A t → y ≤ t * D

noncomputable def P3a.R (A : Set ℕ) (κ t : ℕ) : Finset ℕ

R κ t: residues mod κ of sums of at most t generators.

Equations

• P3a.R A κ t = {r ∈ Finset.range κ | ∃ y ∈ P3a.L A t, y % κ = r}

theorem P3a.mem_R (A : Set ℕ) {κ t r : ℕ} : r ∈ R A κ t ↔ r < κ ∧ ∃ y ∈ L A t, y % κ = r

theorem P3a.R_sub (A : Set ℕ) (κ t : ℕ) : R A κ t ⊆ Finset.range κ

theorem P3a.R_succ (A : Set ℕ) (κ t : ℕ) : R A κ t ⊆ R A κ (t + 1)

theorem P3a.R_mono (A : Set ℕ) (κ : ℕ) {s t : ℕ} (h : s ≤ t) : R A κ s ⊆ R A κ t

theorem P3a.exists_bound (A : Set ℕ) (hfin : (gaps A).Finite) : ∃ (B : ℕ), ∀ (x : ℕ), B < x → x ∈ AddSubmonoid.closure A

Finitely many gaps: everything above some B is in the semigroup.

theorem P3a.exists_mem_mod (A : Set ℕ) (hfin : (gaps A).Finite) {κ r : ℕ} (hr : r < κ) : ∃ x ∈ AddSubmonoid.closure A, x % κ = r

A semigroup with finitely many gaps meets every residue class.

theorem P3a.R_stable (A : Set ℕ) {κ t : ℕ} (hfin : (gaps A).Finite) (h : R A κ (t + 1) = R A κ t) : R A κ t = Finset.range κ

If the residue set stops growing, it is everything.

theorem P3a.R_card (A : Set ℕ) {κ : ℕ} (hκ : 0 < κ) (hfin : (gaps A).Finite) (t : ℕ) : t + 1 ≤ (R A κ t).card ∨ R A κ t = Finset.range κ

The residue set grows by at least one per step until it is everything.

noncomputable def P3a.lev (A : Set ℕ) (κ r : ℕ) : ℕ

The level of a residue: least number of generators reaching it.

Equations

• P3a.lev A κ r = if h : ∃ (t : ℕ), r ∈ P3a.R A κ t then Nat.find h else 0

theorem P3a.R_full (A : Set ℕ) {κ : ℕ} (hκ : 0 < κ) (hfin : (gaps A).Finite) : R A κ (κ - 1) = Finset.range κ

theorem P3a.lev_spec (A : Set ℕ) {κ r : ℕ} (hκ : 0 < κ) (hfin : (gaps A).Finite) (hr : r < κ) (t : ℕ) : lev A κ r ≤ t ↔ r ∈ R A κ t

theorem P3a.sum_lev_le (A : Set ℕ) {κ : ℕ} (hκ : 0 < κ) (hfin : (gaps A).Finite) : ∑ r ∈ Finset.range κ, lev A κ r ≤ ∑ t ∈ Finset.range κ, t

Σ_{r<κ} lev r ≤ Σ_{t<κ} t.

theorem P3a.card_gaps_residue (A : Set ℕ) {κ r y : ℕ} (hκS : κ ∈ AddSubmonoid.closure A) (hfin : (gaps A).Finite) (hy : y ∈ AddSubmonoid.closure A) (hyr : y % κ = r) : κ * {x ∈ hfin.toFinset | x % κ = r}.card + r ≤ y

Gaps in the residue class of r lie below an element y ≡ r of the semigroup.

theorem P3a.genus_le (A : Set ℕ) {D κ : ℕ} (hA : ∀ a ∈ A, a ≤ D) (hfin : (gaps A).Finite) (hκ : 0 < κ) (hκS : κ ∈ AddSubmonoid.closure A) : 2 * genus A ≤ (κ - 1) * (D - 1)

Gap bound (proof of prop:maximo): a semigroup generated in degrees ≤ D, with finitely many gaps and containing κ > 0, has 2·g ≤ (κ−1)(D−1).

theorem P3a.not_all_dvd (A : Set ℕ) (hfin : (gaps A).Finite) {d : ℕ} (hd : 2 ≤ d) : ¬∀ a ∈ A, d ∣ a

If every generator is divisible by d ≥ 2, there are infinitely many gaps.

theorem P3a.genus_le_D (A : Set ℕ) {D : ℕ} (hA : ∀ a ∈ A, a ≤ D) (hfin : (gaps A).Finite) : 2 * genus A ≤ (D - 1) * (D - 2)

prop:maximo, the bound: generated in degrees ≤ D, finitely many gaps ⇒ 2·g ≤ (D−1)(D−2), i.e. δ ≤ (n−1)(n−2)/2 with D = n.

theorem P3a.eq_pair_of_genus_eq (A : Set ℕ) {D : ℕ} (hD : 3 ≤ D) (hA : ∀ a ∈ A, a ≤ D) (hfin : (gaps A).Finite) (heq : 2 * genus A = (D - 1) * (D - 2)) : AddSubmonoid.closure A = AddSubmonoid.closure {D - 1, D}

prop:maximo, the equality case (semigroup part): D ≥ 3, generated in degrees ≤ D, finitely many gaps and 2·g = (D−1)(D−2) ⇒ the semigroup is ⟨D−1, D⟩.

theorem P3a.genus_pair_n {n : ℕ} (hn : 2 ≤ n) : 2 * genus {n - 1, n} = (n - 1) * (n - 2)

The bound is attained: ⟨n−1, n⟩ (n ≥ 2) has 2·g = (n−1)(n−2).