Numerical semigroups generated by powers

TheoremMinimal generators of the tail semigroups of an increasing sequence#●ready to prove

Let \(x_0 < x_1 < x_2 < \cdots\) be a strictly increasing sequence of natural numbers. For \(m \ge 1\) let \(S_m\) be the additive submonoid of \(\mathbb{N}\) generated by \(x_m, x_{m+1}, \ldots\), and let \(\beta(S_m)\) be its set of minimal generators, the nonzero elements of \(S_m\) that are not the sum of two nonzero elements of \(S_m\). For \(k \ge 1\) let \(r_k\) be the least \(m \ge 1\) with \(x_k \in \beta(S_m)\). Then for all integers \(k, n \ge 1\), \(x_k \in \beta(S_n)\) if and only if \(r_k \le n \le k\); and the embedding dimension \(e(S_n) = |\beta(S_n)|\) equals the number of integers \(j \ge 1\) with \(r_j \le n \le j\).

The paper's standing assumption \(\gcd(x_n, x_{n+1}, \ldots) = 1\) is not needed and is dropped.

MetaMathlibExt.mem_minimalGenerators_iff_firstAppearance_le · 15 lines

public theorem_wanted mem_minimalGenerators_iff_firstAppearance_le (x : ℕ → ℕ) (hx : StrictMono x)
    (k n : ℕ) (hk : 1 ≤ k) (hn : 1 ≤ n) :
    (x k ∈ {s | s ∈ AddSubmonoid.closure (x '' Set.Ici n) ∧ s ≠ 0 ∧
        ∀ a ∈ AddSubmonoid.closure (x '' Set.Ici n), ∀ b ∈ AddSubmonoid.closure (x '' Set.Ici n),
          a + b = s → a = 0 ∨ b = 0} ↔
      sInf {m : ℕ | 1 ≤ m ∧ x k ∈ {s | s ∈ AddSubmonoid.closure (x '' Set.Ici m) ∧ s ≠ 0 ∧
        ∀ a ∈ AddSubmonoid.closure (x '' Set.Ici m), ∀ b ∈ AddSubmonoid.closure (x '' Set.Ici m),
          a + b = s → a = 0 ∨ b = 0}} ≤ n ∧ n ≤ k) ∧
    {s | s ∈ AddSubmonoid.closure (x '' Set.Ici n) ∧ s ≠ 0 ∧
        ∀ a ∈ AddSubmonoid.closure (x '' Set.Ici n), ∀ b ∈ AddSubmonoid.closure (x '' Set.Ici n),
          a + b = s → a = 0 ∨ b = 0}.ncard =
      {j : ℕ | 1 ≤ j ∧ sInf {m : ℕ | 1 ≤ m ∧ x j ∈ {s | s ∈ AddSubmonoid.closure (x '' Set.Ici m) ∧
          s ≠ 0 ∧ ∀ a ∈ AddSubmonoid.closure (x '' Set.Ici m),
            ∀ b ∈ AddSubmonoid.closure (x '' Set.Ici m), a + b = s → a = 0 ∨ b = 0}} ≤ n ∧
        n ≤ j}.ncard

Sources

Fabián Arias, Jerson Borja and Jaider Terán, A Note on Numerical Semigroups Generated by k-th Powers, INTEGERS 25 (2025), Article A11, Lemma 1.

TheoremEmbedding dimension bound from linear growth of first appearances#●ready to prove

Let \(x_0 < x_1 < x_2 < \cdots\) be a strictly increasing sequence of natural numbers. For \(m \ge 1\) let \(S_m\) be the additive submonoid of \(\mathbb{N}\) generated by \(x_m, x_{m+1}, \ldots\); call a nonzero element of \(S_m\) that is not the sum of two nonzero elements of \(S_m\) a minimal generator of \(S_m\), and let the embedding dimension \(e(S_m)\) be the number of minimal generators of \(S_m\). For \(k \ge 1\) let \(r_k\) be the least \(m \ge 1\) such that \(x_k\) is a minimal generator of \(S_m\). If \(\alpha > 0\) is a real number with \(r_k \ge \alpha k\) for all \(k \ge 1\), then \(e(S_n) \le \lfloor n / \alpha \rfloor - n + 1\) for all \(n \ge 1\).

The paper's standing assumption \(\gcd(x_n, x_{n+1}, \ldots) = 1\) is not needed and is dropped.

public theorem_wanted embeddingDimension_le_of_firstAppearance_ge (x : ℕ → ℕ) (hx : StrictMono x)
    (α : ℝ) (hα : 0 < α)
    (hr : ∀ k : ℕ, 1 ≤ k → α * k ≤ ((sInf {m : ℕ | 1 ≤ m ∧
      x k ∈ {s | s ∈ AddSubmonoid.closure (x '' Set.Ici m) ∧ s ≠ 0 ∧
        ∀ a ∈ AddSubmonoid.closure (x '' Set.Ici m), ∀ b ∈ AddSubmonoid.closure (x '' Set.Ici m),
          a + b = s → a = 0 ∨ b = 0}} : ℕ) : ℝ))
    (n : ℕ) (hn : 1 ≤ n) :
    ({s | s ∈ AddSubmonoid.closure (x '' Set.Ici n) ∧ s ≠ 0 ∧
        ∀ a ∈ AddSubmonoid.closure (x '' Set.Ici n), ∀ b ∈ AddSubmonoid.closure (x '' Set.Ici n),
          a + b = s → a = 0 ∨ b = 0}.ncard : ℤ) ≤ ⌊(n : ℝ) / α⌋ - n + 1

Sources

Fabián Arias, Jerson Borja and Jaider Terán, A Note on Numerical Semigroups Generated by k-th Powers, INTEGERS 25 (2025), Article A11, Proposition 1.

TheoremFour squares with large nonzero parts#●ready to prove

There is a real constant \(C > 0\) such that every positive integer \(n\) can be written as \(n = a_1^2 + a_2^2 + a_3^2 + a_4^2\) with integers \(a_1, a_2, a_3, a_4\), each of which is either \(0\) or at least \(\sqrt{n} / C\).

public theorem_wanted exists_four_squares_large_parts :
    ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 1 ≤ n → ∃ a : Fin 4 → ℤ,
      (n : ℤ) = ∑ i, a i ^ 2 ∧ ∀ i, a i = 0 ∨ Real.sqrt n / C ≤ a i

Sources

Fabián Arias, Jerson Borja and Jaider Terán, A Note on Numerical Semigroups Generated by k-th Powers, INTEGERS 25 (2025), Article A11, Lemma 2, quoting A. Moscariello.

TheoremDutch–Rickett conductor inequality for a union of generating sets#●ready to prove

For a set \(X\) of natural numbers, let \(\tau(X)\) be the conductor of the additive submonoid \(\langle X \rangle\) of \(\mathbb{N}\) generated by \(X\), the least natural number \(c\) such that every \(j \ge c\) lies in \(\langle X \rangle\). Let \(A\) and \(B\) be nonempty sets of natural numbers such that \(1\) is the only natural number dividing every element of \(A \cup B\), let \(t\) be a natural number dividing every element of \(A\), and let \(C = \{a / t : a \in A\}\) (with \(a / 0 = 0\)). Then

\[\tau(A \cup B) \le t \, \tau(C \cup B) + \tau(B \cup \{t\}).\]

public theorem_wanted conductor_union_le (A B : Set ℕ) (hA : A.Nonempty) (hB : B.Nonempty)
    (hgcd : ∀ g : ℕ, (∀ a ∈ A ∪ B, g ∣ a) → g = 1) (t : ℕ) (ht : ∀ a ∈ A, t ∣ a) :
    sInf {m : ℕ | ∀ j ≥ m, j ∈ AddSubmonoid.closure (A ∪ B)} ≤
      t * sInf {m : ℕ | ∀ j ≥ m, j ∈ AddSubmonoid.closure ((fun a => a / t) '' A ∪ B)} +
        sInf {m : ℕ | ∀ j ≥ m, j ∈ AddSubmonoid.closure (B ∪ {t})}

Sources

Fabián Arias, Jerson Borja and Jaider Terán, A Note on Numerical Semigroups Generated by k-th Powers, INTEGERS 25 (2025), Article A11, Lemma 3, quoting K. Dutch and C. Rickett.

TheoremDutch–Rickett conductor recursion for semigroups of \(k\)-th powers#●ready to prove

Fix an integer \(k \ge 1\). For \(m \ge 1\) let \(S_m\) be the additive submonoid of \(\mathbb{N}\) generated by \(m^k, (m+1)^k, (m+2)^k, \ldots\), and let \(\tau(S_m)\) be its conductor, the least natural number \(c\) such that every \(j \ge c\) lies in \(S_m\). Then for every integer \(n \ge 1\),

\[\tau(S_n) \le 2^k \, \tau(S_{\lceil n/2 \rceil}) + (2^k - 1)(2n)^k.\]

public theorem_wanted conductor_powers_le (n k : ℕ) (hn : 1 ≤ n) (hk : 1 ≤ k) :
    sInf {m : ℕ | ∀ j ≥ m, j ∈ AddSubmonoid.closure ((fun i => i ^ k) '' Set.Ici n)} ≤
      2 ^ k * sInf {m : ℕ | ∀ j ≥ m,
        j ∈ AddSubmonoid.closure ((fun i => i ^ k) '' Set.Ici ((n + 1) / 2))} +
        (2 ^ k - 1) * (2 * n) ^ k

Sources

Fabián Arias, Jerson Borja and Jaider Terán, A Note on Numerical Semigroups Generated by k-th Powers, INTEGERS 25 (2025), Article A11, Proposition 2, inequality (3), quoting K. Dutch and C. Rickett.

TheoremSemigroups of squares have embedding dimension \(O(n)\)#●ready to prove

For \(n \ge 1\) let \(S_n\) be the additive submonoid of \(\mathbb{N}\) generated by \(n^2, (n+1)^2, (n+2)^2, \ldots\), and let \(e(S_n)\) be its embedding dimension, the number of nonzero elements of \(S_n\) that are not the sum of two nonzero elements of \(S_n\). There is a natural number \(C\) with \(e(S_n) \le C n\) for all \(n \ge 1\).

public theorem_wanted embeddingDimension_squares_isBigO :
    ∃ C : ℕ, ∀ n : ℕ, 1 ≤ n →
      {s | s ∈ AddSubmonoid.closure ((fun i => i ^ 2) '' Set.Ici n) ∧ s ≠ 0 ∧
        ∀ a ∈ AddSubmonoid.closure ((fun i => i ^ 2) '' Set.Ici n),
          ∀ b ∈ AddSubmonoid.closure ((fun i => i ^ 2) '' Set.Ici n),
            a + b = s → a = 0 ∨ b = 0}.ncard ≤ C * n

Sources

Fabián Arias, Jerson Borja and Jaider Terán, A Note on Numerical Semigroups Generated by k-th Powers, INTEGERS 25 (2025), Article A11, Theorem 1.

TheoremFrobenius numbers of semigroups of \(k\)-th powers are \(O(n^{k+\varepsilon})\)#●ready to prove

Let \(k \ge 2\) be an integer and \(\varepsilon > 0\) a real number. For \(n \ge 1\) let \(S_n\) be the additive submonoid of \(\mathbb{N}\) generated by \(n^k, (n+1)^k, (n+2)^k, \ldots\). Then there is a real constant \(K\) such that for every \(n \ge 1\), if \(S_n\) has a Frobenius number \(F\) (the largest natural number not in \(S_n\)), then \(F \le K n^{k + \varepsilon}\).

Since \(S_1 = \mathbb{N}\) has no Frobenius number, the case \(n = 1\) is vacuous.

public theorem_wanted frobeniusNumber_powers_isBigO (k : ℕ) (hk : 2 ≤ k) (ε : ℝ) (hε : 0 < ε) :
    ∃ K : ℝ, ∀ n : ℕ, 1 ≤ n → ∀ F : ℕ, FrobeniusNumber F ((fun i => i ^ k) '' Set.Ici n) →
      (F : ℝ) ≤ K * (n : ℝ) ^ ((k : ℝ) + ε)

Sources

Fabián Arias, Jerson Borja and Jaider Terán, A Note on Numerical Semigroups Generated by k-th Powers, INTEGERS 25 (2025), Article A11, Theorem 2.

7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.