Frobenius numbers of consecutive star numbers

DefinitionStar numbers#✓fully proved

For a natural number \(n\), the \(n\)-th star number is \(S_n = 6n(n-1)+1\).

def star (n : ℕ) : ℕ :=
  6 * n * (n - 1) + 1
Used by 4
Used byFrobenius numbers of three consecutive star numbers for \(6 \le n \le 9\) · Frobenius numbers of three consecutive star numbers for \(n \ge 10\) · Three consecutive star numbers are relatively prime · Representation count for three consecutive star numbers

DefinitionRepresentation count for three consecutive star numbers#✓fully proved

Write \(S_m\) for the \(m\)-th star number \(6m(m-1)+1\). For natural numbers \(n\) and \(N\), the representation count of \(N\) is the number of triples \((x, y, z)\) of natural numbers with \(x S_n + y S_{n+1} + z S_{n+2} = N\).

The star numbers are positive, so there are only finitely many such triples.

noncomputable def starRepCount (n N : ℕ) : ℕ :=
  Nat.card {xyz : ℕ × ℕ × ℕ //
    xyz.1 * star n + xyz.2.1 * star (n + 1) +
      xyz.2.2 * star (n + 2) = N}
Uses 1 · Used by 2
Statement usesStar numbers
Used by\(p\)-Frobenius number of three consecutive star numbers · \(p\)-Sylvester number of three consecutive star numbers

Definition\(p\)-Frobenius number of three consecutive star numbers#✓fully proved

Write \(S_m\) for the \(m\)-th star number \(6m(m-1)+1\). For natural numbers \(p\), \(n\) and \(g\), \(g\) is the \(p\)-Frobenius number of \(S_n, S_{n+1}, S_{n+2}\) when at most \(p\) triples \((x, y, z)\) of natural numbers satisfy \(x S_n + y S_{n+1} + z S_{n+2} = g\), and every natural number \(N > g\) has more than \(p\) triples \((x, y, z)\) of natural numbers with \(x S_n + y S_{n+1} + z S_{n+2} = N\).

def IsPFrobeniusStarNumber (p n g : ℕ) : Prop :=
  starRepCount n g ≤ p ∧ ∀ N : ℕ, g < N → p < starRepCount n N
Uses 1 · Used by 2
Statement usesRepresentation count for three consecutive star numbers
Used byFrobenius numbers of three consecutive star numbers for \(6 \le n \le 9\) · Frobenius numbers of three consecutive star numbers for \(n \ge 10\)

Definition\(p\)-Sylvester number of three consecutive star numbers#✓fully proved

Write \(S_m\) for the \(m\)-th star number \(6m(m-1)+1\). For natural numbers \(p\) and \(n\), the \(p\)-Sylvester number of \(S_n, S_{n+1}, S_{n+2}\) is the number of natural numbers \(N\) for which at most \(p\) triples \((x, y, z)\) of natural numbers satisfy \(x S_n + y S_{n+1} + z S_{n+2} = N\).

For \(n \ge 1\) the three star numbers are relatively prime, so this set of natural numbers is finite.

noncomputable def pSylvesterStarCount (p n : ℕ) : ℕ :=
  Nat.card {N : ℕ // starRepCount n N ≤ p}
Uses 1 · Used by 3
Statement usesRepresentation count for three consecutive star numbers
Used by\(1\)-Sylvester number of three consecutive star numbers · \(2\)-Sylvester number of three consecutive star numbers · \(0\)-Sylvester number of three consecutive star numbers

TheoremThree consecutive star numbers are relatively prime#●ready to prove

Write \(S_m\) for the \(m\)-th star number \(6m(m-1)+1\). For every natural number \(n \ge 1\), \(\gcd(S_n, S_{n+1}, S_{n+2}) = 1\).

theorem_wanted gcd_star_succ_succ
    (n : ℕ) (hn : 1 ≤ n) :
    Nat.gcd (Nat.gcd (star n) (star (n + 1))) (star (n + 2)) = 1
Sources
  • "On p-Frobenius Numbers for the Numerical Semigroups Generated by Three Consecutive Star Numbers", Lemma 2.
Uses 1
Statement usesStar numbers

TheoremFrobenius numbers of three consecutive star numbers for \(6 \le n \le 9\)#●ready to prove

Write \(S_m\) for the \(m\)-th star number \(6m(m-1)+1\). For natural numbers \(n\) and \(p\) with \(6 \le n \le 9\) and \(p \in \{0, 1, 2\}\), there is a natural number \(g\) such that at most \(p\) triples \((x, y, z)\) of natural numbers satisfy \(x S_n + y S_{n+1} + z S_{n+2} = g\), every natural number larger than \(g\) has more than \(p\) such triples, and \(g = 2n S_{n+1} + (p + 2) n S_{n+2} - S_n\). That is, the \(p\)-Frobenius number of \(S_n, S_{n+1}, S_{n+2}\) is \(2n S_{n+1} + (p + 2) n S_{n+2} - S_n\).

theorem_wanted exists_isPFrobeniusNumber_star_of_le_nine
    (n p : ℕ) (hn : 6 ≤ n) (hn9 : n ≤ 9) (hp : p = 0 ∨ p = 1 ∨ p = 2) :
    ∃ g : ℕ, IsPFrobeniusStarNumber p n g ∧
      (g : ℤ) = 2 * n * star (n + 1) + (p + 2) * n * star (n + 2) -
        star n
Sources
  • "On p-Frobenius Numbers for the Numerical Semigroups Generated by Three Consecutive Star Numbers", Theorem 1.
Uses 2
Statement uses\(p\)-Frobenius number of three consecutive star numbers · Star numbers

TheoremFrobenius numbers of three consecutive star numbers for \(n \ge 10\)#●ready to prove

Write \(S_m\) for the \(m\)-th star number \(6m(m-1)+1\). For natural numbers \(n\) and \(p\) with \(n \ge 10\) and \(p \in \{0, 1, 2\}\), there is a natural number \(g\) such that at most \(p\) triples \((x, y, z)\) of natural numbers satisfy \(x S_n + y S_{n+1} + z S_{n+2} = g\), every natural number larger than \(g\) has more than \(p\) such triples, and \(g = (2n - 11) S_{n+1} + (p + 3) n S_{n+2} - S_n\). That is, the \(p\)-Frobenius number of \(S_n, S_{n+1}, S_{n+2}\) is \((2n - 11) S_{n+1} + (p + 3) n S_{n+2} - S_n\).

theorem_wanted exists_isPFrobeniusNumber_star_of_ten_le
    (n p : ℕ) (hn : 10 ≤ n) (hp : p = 0 ∨ p = 1 ∨ p = 2) :
    ∃ g : ℕ, IsPFrobeniusStarNumber p n g ∧
      (g : ℤ) = (2 * n - 11) * star (n + 1) + (p + 3) * n * star (n + 2) -
        star n
Sources
  • "On p-Frobenius Numbers for the Numerical Semigroups Generated by Three Consecutive Star Numbers", Theorem 1.
Uses 2
Statement uses\(p\)-Frobenius number of three consecutive star numbers · Star numbers

Theorem\(0\)-Sylvester number of three consecutive star numbers#●ready to prove

Write \(S_m\) for the \(m\)-th star number \(6m(m-1)+1\). For every natural number \(n \ge 6\), the number of natural numbers that cannot be written as \(x S_n + y S_{n+1} + z S_{n+2}\) with \(x, y, z\) natural numbers is \(n(15n^2 + 8n + 7)\).

theorem_wanted pSylvesterCount_zero_star
    (n : ℕ) (hn : 6 ≤ n) :
    pSylvesterStarCount 0 n =
      n * (15 * n ^ 2 + 8 * n + 7)
Sources
  • "On p-Frobenius Numbers for the Numerical Semigroups Generated by Three Consecutive Star Numbers", Theorem 2.
Uses 1
Statement uses\(p\)-Sylvester number of three consecutive star numbers

Theorem\(1\)-Sylvester number of three consecutive star numbers#●ready to prove

Write \(S_m\) for the \(m\)-th star number \(6m(m-1)+1\). For every natural number \(n \ge 6\), the number of natural numbers \(N\) for which at most one triple \((x, y, z)\) of natural numbers satisfies \(x S_n + y S_{n+1} + z S_{n+2} = N\) is \(25n^3 + 23n^2 + 14n + 1\).

theorem_wanted pSylvesterCount_one_star
    (n : ℕ) (hn : 6 ≤ n) :
    pSylvesterStarCount 1 n =
      25 * n ^ 3 + 23 * n ^ 2 + 14 * n + 1
Sources
  • "On p-Frobenius Numbers for the Numerical Semigroups Generated by Three Consecutive Star Numbers", Theorem 2.
Uses 1
Statement uses\(p\)-Sylvester number of three consecutive star numbers

Theorem\(2\)-Sylvester number of three consecutive star numbers#●ready to prove

Write \(S_m\) for the \(m\)-th star number \(6m(m-1)+1\). For every natural number \(n \ge 6\), the number of natural numbers \(N\) for which at most two triples \((x, y, z)\) of natural numbers satisfy \(x S_n + y S_{n+1} + z S_{n+2} = N\) is \(33n^3 + 35n^2 + 20n + 2\).

theorem_wanted pSylvesterCount_two_star
    (n : ℕ) (hn : 6 ≤ n) :
    pSylvesterStarCount 2 n =
      33 * n ^ 3 + 35 * n ^ 2 + 20 * n + 2
Sources
  • "On p-Frobenius Numbers for the Numerical Semigroups Generated by Three Consecutive Star Numbers", Theorem 2.
Uses 1
Statement uses\(p\)-Sylvester number of three consecutive star numbers
4 fully proved6 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.