Binomid indices and generalized binomial coefficients

DefinitionBinomid index#✓fully proved

An infinite binomid index is a sequence \((e_1, e_2, \dots)\) of nonnegative integers such that \(\sum_{i=n-k+1}^{n} e_i \ge \sum_{i=1}^{k} e_i\) for all \(1 \le k \le n\).

public def IsBinomidIndex (η : ℕ → ℕ) : Prop :=
  ∀ k n : ℕ, k ≤ n → ∑ i ∈ Finset.range k, η i ≤ ∑ i ∈ Finset.Ico (n - k) n, η i

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53; definition as restated in arXiv:2505.20018, Section 1.

Used by 13

Used byAverages of a binomid index · The upper average of a binomid index is the supremum of its averages · Nomid coefficients of binomid indices that are not lex-minimal extensions · Atomic binomid index · The constant sequence \(1\) is atomic · Constant sequences are binomid indices · Partial-sum characterization of binomid indices · Monotone sequences are binomid indices · The Average Condition gives eventually periodic lex-minimal extensions · Lex-minimal extension · Periodic binomid indices are lex-minimal extensions · The zero sequence is lex-minimal · Summands of a lex-minimal extension are lex-minimal

TheoremConstant sequences are binomid indices#✓fully proved

For every natural number \(c\), the constant sequence \((c, c, c, \dots)\) is a binomid index.

public theorem isBinomidIndex_const (c : ℕ) : IsBinomidIndex fun _ => c

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53.

Uses 1 · Used by 2

Statement usesBinomid index

Used byThe constant sequence \(1\) is atomic · The zero sequence is lex-minimal

DefinitionLex-minimal extension#✓fully proved

Let \(e = (e_1, e_2, \dots)\) be a sequence of nonnegative integers and \(m \ge 0\). Then \(e\) is the lex-minimal extension of \((e_1, \dots, e_m)\) when \(e\) is an infinite binomid index and, for every infinite binomid index \(g\) with \(g_i = e_i\) for all \(i \le m\), either \(g = e\) or \(e\) is lexicographically smaller than \(g\): there is a \(j\) with \(e_i = g_i\) for all \(i < j\) and \(e_j < g_j\).

public def IsLexMinimalExtensionOf (η : ℕ → ℕ) (m : ℕ) : Prop :=
  IsBinomidIndex η ∧ ∀ γ : ℕ → ℕ, IsBinomidIndex γ → (∀ i < m, γ i = η i) →
    η = γ ∨ ∃ j, (∀ i < j, η i = γ i) ∧ η j < γ j

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53; definition as restated in arXiv:2505.20018, Section 1.

Uses 1 · Used by 19

Statement usesBinomid index

Used byThe largest of the first \(m\) averages is the largest average · Spans of lex-minimal extensions of a fixed length are finitely presented · Partial sums of a lex-minimal extension solve a knapsack problem · Lex-minimal extensions have a nomid coefficient equal to one · Late partial sums of a lex-minimal extension split · A preperiod bound for lex-minimal extensions · Spans of lex-minimal extensions of a fixed length are finitely generated · Every index with maximal average is a multiple of the gcd of those up to \(m\) · The gcd of the maximizing indices divides the minimal period · The monoid of lex-minimal extensions is a directed union · Basis of the span of the lex-minimal extensions of length \(k\) · Partial-sum characterization of binomid indices · Minimal period of a lex-minimal extension · Lex-minimal extensions · Partial-sum criterion for lex-minimal extensions · The lex-minimal extension is computed greedily · Monotone finite binomid indices extend periodically · The zero sequence is lex-minimal · Summands of a lex-minimal extension are lex-minimal

DefinitionLex-minimal extensions#✓fully proved

A sequence \(e = (e_1, e_2, \dots)\) of nonnegative integers is a lex-minimal extension when, for some \(m \ge 0\), it is the lex-minimal extension of \((e_1, \dots, e_m)\). The set of all lex-minimal extensions is denoted \(L\).

public def IsLexMinimalExtension (η : ℕ → ℕ) : Prop :=
  ∃ m : ℕ, IsLexMinimalExtensionOf η m

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53.

Uses 1 · Used by 9

Statement usesLex-minimal extension

Used byLex-minimal extensions are closed under addition · A lex-minimal extension periodic from its second entry is periodic · Lex-minimal extensions satisfy the Average Condition · Distinct shifts of lex-minimal extensions meet only in zero · The monoid of lex-minimal extensions is a directed union · Nomid coefficients of binomid indices that are not lex-minimal extensions · Basis of the monoid of lex-minimal extensions · The Average Condition gives eventually periodic lex-minimal extensions · Periodic binomid indices are lex-minimal extensions

TheoremThe zero sequence is lex-minimal#✓fully proved

For every \(m \ge 0\), the zero sequence \((0, 0, \dots)\) is the lex-minimal extension of its first \(m\) entries.

public theorem isLexMinimalExtensionOf_zero (m : ℕ) :
    IsLexMinimalExtensionOf (fun _ => 0) m

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53.

Uses 3

Statement usesLex-minimal extension

Proof usesBinomid index · Constant sequences are binomid indices

DefinitionRight shift of a sequence#✓fully proved

For a natural number \(l\), the right shift \(\sigma^l\) sends a sequence \(\eta = (e_1, e_2, \dots)\) of nonnegative integers to the sequence \((0, \dots, 0, e_1, e_2, \dots)\) obtained by prepending \(l\) zeros: its first \(l\) entries are \(0\) and its \((l + i)\)-th entry is \(e_i\) for every \(i \ge 1\).

public def binomidShift (l : ℕ) (η : ℕ → ℕ) : ℕ → ℕ :=
  fun i => if i < l then 0 else η (i - l)

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53; definition as restated in arXiv:2505.20018, Section 1.

Used by 2

Used byDistinct shifts of lex-minimal extensions meet only in zero · Shifting by zero places is the identity

TheoremShifting by zero places is the identity#✓fully proved

For every sequence \(\eta\) of nonnegative integers, \(\sigma^0(\eta) = \eta\), where \(\sigma^l\) is the right shift that prepends \(l\) zeros.

public theorem binomidShift_zero (η : ℕ → ℕ) : binomidShift 0 η = η

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53.

Uses 1

Statement usesRight shift of a sequence

TheoremMonotone sequences are binomid indices#●ready to prove

Every non-decreasing sequence \(e_1 \le e_2 \le \cdots\) of nonnegative integers is an infinite binomid index.

public theorem_wanted isBinomidIndex_of_monotone {η : ℕ → ℕ} (hη : Monotone η) :
    IsBinomidIndex η

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Proposition 1.

Uses 1

Statement usesBinomid index

TheoremPartial-sum characterization of binomid indices#●ready to prove

Let \(\eta = (e_1, e_2, \dots)\) be a sequence of nonnegative integers with partial sums \(s_n = e_1 + \dots + e_n\) (so \(s_0 = 0\)). Then \(\eta\) is a binomid index if and only if \(s_{n-k} + s_k \le s_n\) for all \(k\) and \(n\) with \(1 \le k < n\). Moreover, for every \(m\), if \(\eta\) is the lex-minimal extension of its first \(m\) entries, then for every \(n > m\)

\[s_n = \max_{1 \le k < n} (s_{n-k} + s_k),\]

where the maximum over the empty range (for \(n = 1\)) is taken to be \(0\).

public theorem_wanted isBinomidIndex_iff_partialSum (η : ℕ → ℕ) :
    (IsBinomidIndex η ↔ ∀ k n : ℕ, 1 ≤ k → k < n →
      ∑ i ∈ Finset.range (n - k), η i + ∑ i ∈ Finset.range k, η i
        ≤ ∑ i ∈ Finset.range n, η i) ∧
    ∀ m : ℕ, IsLexMinimalExtensionOf η m → ∀ n : ℕ, m < n →
      ∑ i ∈ Finset.range n, η i
        = (Finset.Ico 1 n).sup fun k =>
            ∑ i ∈ Finset.range (n - k), η i + ∑ i ∈ Finset.range k, η i

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Lemma 1.

Uses 2

Statement usesBinomid index · Lex-minimal extension

TheoremMonotone finite binomid indices extend periodically#●ready to prove

Let \(m \ge 1\) and let \(e_1 \le e_2 \le \cdots \le e_m\) be nonnegative integers. Then the periodic sequence \((e_1, \dots, e_m, e_1, \dots, e_m, \dots)\) is the lex-minimal extension of \((e_1, \dots, e_m)\).

A non-decreasing finite sequence is automatically a finite binomid index.

public theorem_wanted isLexMinimalExtensionOf_periodic_of_monotoneOn {m : ℕ}
    (hm : 0 < m) {e : ℕ → ℕ} (he : MonotoneOn e (Set.Iio m)) :
    IsLexMinimalExtensionOf (fun i => e (i % m)) m

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Proposition 3.

Uses 1

Statement usesLex-minimal extension

TheoremA lex-minimal extension periodic from its second entry is periodic#●ready to prove

Let \(\eta = (e_1, e_2, \dots)\) be a lex-minimal extension and let \(p \ge 1\). If \(e_{i+p} = e_i\) for every \(i \ge 2\), then \(e_{1+p} = e_1\), so the whole sequence \(\eta\) is periodic with period \(p\).

public theorem_wanted IsLexMinimalExtension.apply_period_eq_apply_zero {η : ℕ → ℕ}
    (hη : IsLexMinimalExtension η) {p : ℕ} (hp : 0 < p)
    (hper : ∀ i, 1 ≤ i → η (i + p) = η i) : η p = η 0

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Proposition 4.

Uses 1

Statement usesLex-minimal extensions

TheoremPeriodic binomid indices are lex-minimal extensions#●ready to prove

If an infinite binomid index \(e = (e_1, e_2, \dots)\) is periodic, that is, there is \(p \ge 1\) with \(e_{i+p} = e_i\) for all \(i\), then \(e\) is a lex-minimal extension: it is the lex-minimal extension of \((e_1, \dots, e_m)\) for some \(m \ge 0\).

public theorem_wanted isLexMinimalExtension_of_periodic {η : ℕ → ℕ}
    (hη : IsBinomidIndex η) {p : ℕ} (hp : 0 < p) (hper : ∀ i, η (i + p) = η i) :
    IsLexMinimalExtension η

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Proposition 5.

Uses 2

Statement usesBinomid index · Lex-minimal extensions

TheoremLex-minimal extensions are closed under addition#●ready to prove

If \(\eta_1\) and \(\eta_2\) are lex-minimal extensions, then their componentwise sum \(\eta_1 + \eta_2\) is a lex-minimal extension.

Since the zero sequence is also a lex-minimal extension, the set \(L\) of lex-minimal extensions is a monoid under componentwise addition.

public theorem_wanted IsLexMinimalExtension.add {η₁ η₂ : ℕ → ℕ}
    (h₁ : IsLexMinimalExtension η₁) (h₂ : IsLexMinimalExtension η₂) :
    IsLexMinimalExtension (η₁ + η₂)

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Corollary 1.

Uses 1

Statement usesLex-minimal extensions

TheoremDistinct shifts of lex-minimal extensions meet only in zero#●ready to prove

Let \(L\) be the set of lex-minimal extensions, and for a natural number \(l\) let \(\sigma^l\) be the right shift that prepends \(l\) zeros to a sequence. For natural numbers \(l \neq m\), \(\sigma^l(L) \cap \sigma^m(L) = \{(0, 0, 0, \dots)\}\): the only sequence in both images is the zero sequence.

public theorem_wanted binomidShift_image_inter_eq_zero {l m : ℕ} (hlm : l ≠ m) :
    binomidShift l '' {η | IsLexMinimalExtension η}
        ∩ binomidShift m '' {η | IsLexMinimalExtension η}
      = {fun _ => 0}

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Proposition 6.

Uses 2

Statement usesLex-minimal extensions · Right shift of a sequence

TheoremPrimes divide all inner binomial coefficients of infinitely many rows#●ready to prove

For every prime \(p\) there are infinitely many natural numbers \(n\) such that \(p\) divides the binomial coefficient \(\binom{n}{k}\) for every \(k\) with \(1 \le k < n\).

public theorem_wanted infinite_setOf_prime_dvd_choose {p : ℕ} (hp : p.Prime) :
    {n : ℕ | ∀ k, 1 ≤ k → k < n → p ∣ n.choose k}.Infinite

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Corollary 3.

TheoremPrimes divide all inner Fibonomial coefficients of infinitely many rows#●ready to prove

Let \(F_n\) be the Fibonacci numbers and \(F_n! = F_1 F_2 \cdots F_n\) the Fibonacci factorial. For every prime \(p\) there are infinitely many natural numbers \(n\) such that for every \(k\) with \(1 \le k < n\) the Fibonomial coefficient \(F_n! / (F_k! \, F_{n-k}!)\) is an integer multiple of \(p\).

public theorem_wanted infinite_setOf_prime_dvd_fibonomial {p : ℕ} (hp : p.Prime) :
    {n : ℕ | ∀ k, 1 ≤ k → k < n → ∃ z : ℤ,
      fibonacciFactorial n / (fibonacciFactorial k * fibonacciFactorial (n - k))
        = (p : ℚ) * z}.Infinite

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Corollary 4.

Uses 1

Statement usesFibonacci factorial

TheoremThe lex-minimal extension is computed greedily#●ready to prove

Let \(m \ge 1\) and let \(f = (f_1, f_2, \dots)\) be a sequence of nonnegative integers whose first \(m\) entries form a finite binomid index, that is, \(\sum_{i=n-k+1}^{n} f_i \ge \sum_{i=1}^{k} f_i\) for all \(1 \le k \le n \le m\). Suppose that for every \(n > m\) the entry \(f_n\) equals the maximum, over \(1 \le k < n\), of the integers \(\sum_{i=1}^{k} f_i - \sum_{i=n-k+1}^{n-1} f_i\). Then \(f\) is the lex-minimal extension of \((f_1, \dots, f_m)\).

The differences are taken in the integers and may be negative; the condition says that \(f_n + \sum_{i=n-k+1}^{n-1} f_i \ge \sum_{i=1}^{k} f_i\) for every \(1 \le k < n\), with equality for some such \(k\).

public theorem_wanted isLexMinimalExtensionOf_of_greedy {m : ℕ} (hm : 0 < m) {f : ℕ → ℕ}
    (hpre : ∀ k n : ℕ, k ≤ n → n ≤ m →
      ∑ i ∈ Finset.range k, f i ≤ ∑ i ∈ Finset.Ico (n - k) n, f i)
    (hle : ∀ j, m ≤ j → ∀ k, 1 ≤ k → k ≤ j →
      ∑ i ∈ Finset.range k, f i ≤ f j + ∑ i ∈ Finset.Ico (j + 1 - k) j, f i)
    (hex : ∀ j, m ≤ j → ∃ k, 1 ≤ k ∧ k ≤ j ∧
      ∑ i ∈ Finset.range k, f i = f j + ∑ i ∈ Finset.Ico (j + 1 - k) j, f i) :
    IsLexMinimalExtensionOf f m

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Proposition 2.

Uses 1

Statement usesLex-minimal extension

TheoremLex-minimal extensions have a nomid coefficient equal to one#●ready to prove

Let \(m \ge 1\), let \(\eta = (e_1, e_2, \dots)\) be the lex-minimal extension of its first \(m\) entries, and let \(p\) be a prime. Write \(f_i = p^{e_i}\) for \(i \ge 1\) and, for \(1 \le k \le n\), let \([n, k]_f = \frac{f_n f_{n-1} \cdots f_{n-k+1}}{f_k f_{k-1} \cdots f_1}\) be the \(f\)-nomid coefficient, the generalized binomial coefficient of \(f\). Then for every \(n > m\) there is some \(k\) with \(1 \le k < n\) and \([n, k]_f = 1\).

public theorem_wanted IsLexMinimalExtensionOf.exists_nomid_eq_one {η : ℕ → ℕ} {m : ℕ}
    (hm : 0 < m) (hη : IsLexMinimalExtensionOf η m) {p : ℕ} (hp : p.Prime) {n : ℕ}
    (hn : m < n) :
    ∃ k, 1 ≤ k ∧ k < n ∧
      generalizedBinomialCoefficient (fun i => p ^ η (i - 1)) k (n - k) = 1

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Corollary 2.

Uses 2

Statement usesLex-minimal extension · Generalized binomial coefficient

TheoremNomid coefficients of binomid indices that are not lex-minimal extensions#●ready to prove

Let \(\mu = (e_1, e_2, \dots)\) be a binomid index such that for no \(m\) is \(\mu\) the lex-minimal extension of its first \(m\) entries, and let \(p\) be a prime. Write \(f_i = p^{e_i}\) for \(i \ge 1\) and let \([n, k]_f = \frac{f_n f_{n-1} \cdots f_{n-k+1}}{f_k f_{k-1} \cdots f_1}\) be the \(f\)-nomid coefficient. Then there are infinitely many natural numbers \(n\) such that for every \(k\) with \(1 \le k < n\) the coefficient \([n, k]_f\) is an integer multiple of \(p\).

public theorem_wanted infinite_setOf_prime_dvd_nomid_of_not_isLexMinimalExtension
    {μ : ℕ → ℕ} (hμ : IsBinomidIndex μ) (hlex : ¬ IsLexMinimalExtension μ) {p : ℕ}
    (hp : p.Prime) :
    {n : ℕ | ∀ k, 1 ≤ k → k < n → ∃ z : ℤ,
      generalizedBinomialCoefficient (fun i => p ^ μ (i - 1)) k (n - k) = (p : ℚ) * z}.Infinite

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Corollary 2.

Uses 3

Statement usesBinomid index · Lex-minimal extensions · Generalized binomial coefficient

DefinitionInitial averages of a sequence#✓fully proved

For a sequence \(\eta = (e_1, e_2, \dots)\) of nonnegative integers and \(i \ge 1\), the average \(A_{i,0}(\eta)\) is the rational number \(s_i / i\), where \(s_i = e_1 + \dots + e_i\) is the sum of the first \(i\) entries; for \(i = 0\) the value is \(A_{0,0}(\eta) = 0\).

public def binomidAverage (η : ℕ → ℕ) (i : ℕ) : ℚ :=
  ((∑ l ∈ Finset.range i, η l : ℕ) : ℚ) / i

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Section 3; the same average is the sequence Ave(η) of Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Section 2.

Used by 12

Used byThe Average Condition · Constant sequences satisfy the Average Condition · Averages of a constant sequence · The largest of the first \(m\) averages is the largest average · The first average is the first entry · Averages of a binomid index · Upper average of a sequence · Upper average of a constant sequence · The upper average of a binomid index is the supremum of its averages · Every index with maximal average is a multiple of the gcd of those up to \(m\) · Indices of maximal average · Maximal-average indices for \(m = 1\)

TheoremAverages of a constant sequence#✓fully proved

For every natural number \(c\) and every \(i \ge 1\), the average \(A_{i,0}\) of the first \(i\) entries of the constant sequence \((c, c, c, \dots)\) equals \(c\).

public theorem binomidAverage_const (c : ℕ) {i : ℕ} (hi : 1 ≤ i) :
    binomidAverage (fun _ => c) i = c

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Section 3.

Uses 1 · Used by 2

Statement usesInitial averages of a sequence

Used byConstant sequences satisfy the Average Condition · Upper average of a constant sequence

DefinitionUpper average of a sequence#✓fully proved

For a sequence \(\eta = (e_1, e_2, \dots)\) of nonnegative integers with partial sums \(s_i = e_1 + \dots + e_i\) and averages \(A_{i,0}(\eta) = s_i / i\), the upper average of \(\eta\) is \(A_0(\eta) = \limsup_{i \to \infty} A_{i,0}(\eta)\), taken in the extended real numbers; it is \(+\infty\) when \(s_i / i\) is unbounded.

public noncomputable def binomidUpperAverage (η : ℕ → ℕ) : EReal :=
  Filter.limsup (fun i => ((binomidAverage η i : ℝ) : EReal)) Filter.atTop

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Section 3.

Uses 1 · Used by 4

Statement usesInitial averages of a sequence

Used byThe Average Condition · Constant sequences satisfy the Average Condition · Upper average of a constant sequence · The upper average of a binomid index is the supremum of its averages

TheoremUpper average of a constant sequence#✓fully proved

For every natural number \(c\), the upper average \(A_0\) of the constant sequence \((c, c, c, \dots)\) equals \(c\).

public theorem binomidUpperAverage_const (c : ℕ) :
    binomidUpperAverage (fun _ => c) = ((c : ℝ) : EReal)

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Section 3.

Uses 3 · Used by 1

Statement usesUpper average of a sequence

Proof usesInitial averages of a sequence · Averages of a constant sequence

Used byConstant sequences satisfy the Average Condition

DefinitionThe Average Condition#✓fully proved

A sequence \(\eta = (e_1, e_2, \dots)\) of nonnegative integers satisfies the Average Condition when its upper average \(A_0(\eta)\), the limit superior as \(n \to \infty\) of the averages \(A_{n,0}(\eta) = (e_1 + \dots + e_n)/n\) taken in the extended real line, equals \(A_{i,0}(\eta)\) for some \(i \ge 1\).

public def BinomidAverageCondition (η : ℕ → ℕ) : Prop :=
  ∃ i, 1 ≤ i ∧ binomidUpperAverage η = ((binomidAverage η i : ℝ) : EReal)

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Lemma 3.

Uses 2 · Used by 3

Statement usesInitial averages of a sequence · Upper average of a sequence

Used byLex-minimal extensions satisfy the Average Condition · Constant sequences satisfy the Average Condition · The Average Condition gives eventually periodic lex-minimal extensions

TheoremConstant sequences satisfy the Average Condition#✓fully proved

For every natural number \(c\), the constant sequence \((c, c, c, \dots)\) satisfies the Average Condition.

public theorem binomidAverageCondition_const (c : ℕ) :
    BinomidAverageCondition fun _ => c

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Lemma 3.

Uses 5

Statement usesThe Average Condition

Proof usesInitial averages of a sequence · Averages of a constant sequence · Upper average of a sequence · Upper average of a constant sequence

TheoremAverages of a binomid index#●ready to prove

Let \(\eta = (e_1, e_2, \dots)\) be a binomid index, write \(s_n = e_1 + \dots + e_n\), and for \(i \ge 1\) and \(l \ge 0\) let \(A_{i,l} = (s_{i+l} - s_l)/i\) be the average of \(e_{l+1}, \dots, e_{l+i}\). Then for all \(i, l \ge 1\): \(A_{i,l} \ge A_{i,0}\); \(A_{ki,0} \ge A_{i,0}\) for every \(k \ge 1\); and \(A_{i+l,0} = \frac{i}{i+l} A_{i,l} + \frac{l}{l+i} A_{l,0}\).

public theorem_wanted IsBinomidIndex.binomidAverage_props {η : ℕ → ℕ} (hη : IsBinomidIndex η)
    {i l : ℕ} (hi : 1 ≤ i) (hl : 1 ≤ l) :
    binomidAverage η i ≤ ((∑ j ∈ Finset.Ico l (i + l), η j : ℕ) : ℚ) / i ∧
      (∀ k, 1 ≤ k → binomidAverage η i ≤ binomidAverage η (k * i)) ∧
      binomidAverage η (i + l) =
        (i : ℚ) / (i + l) * (((∑ j ∈ Finset.Ico l (i + l), η j : ℕ) : ℚ) / i) +
          (l : ℚ) / (l + i) * binomidAverage η l

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Lemma 2.

Uses 2

Statement usesBinomid index · Initial averages of a sequence

TheoremThe upper average of a binomid index is the supremum of its averages#●ready to prove

Let \(\eta\) be a binomid index, let \(s_i\) be the sum of its first \(i\) entries, let \(A_{i,0}(\eta) = s_i / i\) for \(i \ge 1\), and let \(A_0(\eta) = \limsup_{i \to \infty} A_{i,0}(\eta)\) be its upper average. Then, in the extended real numbers, \(A_0(\eta) = \sup_{i \ge 1} A_{i,0}(\eta)\).

public theorem_wanted IsBinomidIndex.binomidUpperAverage_eq_iSup {η : ℕ → ℕ}
    (hη : IsBinomidIndex η) :
    binomidUpperAverage η = ⨆ i : ℕ, ⨆ (_ : 1 ≤ i), ((binomidAverage η i : ℝ) : EReal)

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Lemma 2.

Uses 3

Statement usesBinomid index · Initial averages of a sequence · Upper average of a sequence

TheoremLex-minimal extensions satisfy the Average Condition#●ready to prove

Every lex-minimal extension satisfies the Average Condition.

public theorem_wanted IsLexMinimalExtension.binomidAverageCondition {η : ℕ → ℕ}
    (hη : IsLexMinimalExtension η) : BinomidAverageCondition η

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Lemma 3.

Uses 2

Statement usesThe Average Condition · Lex-minimal extensions

TheoremThe Average Condition gives eventually periodic lex-minimal extensions#●ready to prove

If an infinite binomid index \(e = (e_1, e_2, \dots)\) satisfies the Average Condition, then \(e\) is a lex-minimal extension, that is, the lex-minimal extension of \((e_1, \dots, e_m)\) for some \(m \ge 0\), and \(e\) is eventually periodic: there are \(N\) and \(p \ge 1\) such that \(e_{n+p} = e_n\) for all \(n \ge N\).

public theorem_wanted IsBinomidIndex.isLexMinimalExtension_and_eventually_periodic
    {η : ℕ → ℕ} (hη : IsBinomidIndex η) (hac : BinomidAverageCondition η) :
    IsLexMinimalExtension η ∧ ∃ N p : ℕ, 0 < p ∧ ∀ n, N ≤ n → η (n + p) = η n

Sources

• Caalim and Tanaka, Lexicographically Minimal Extension of a Finite Binomid Index, INTEGERS 24 (2024), Article A53, Theorem 1.

Uses 3

Statement usesThe Average Condition · Binomid index · Lex-minimal extensions

TheoremThe first average is the first entry#✓fully proved

For every sequence \(\eta = (e_1, e_2, \dots)\) of nonnegative integers, the initial average \(A_{1,0}(\eta)\) of its first entry equals \(e_1\).

public theorem binomidAverage_one (η : ℕ → ℕ) : binomidAverage η 1 = η 0

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Section 2.

Uses 1

Statement usesInitial averages of a sequence

DefinitionIndices of maximal average#✓fully proved

For a sequence \(\eta = (e_1, e_2, \dots)\) of nonnegative integers and \(m \ge 0\), let \(A_i = (e_1 + \dots + e_i)/i\) be the average of the first \(i\) entries of \(\eta\). The set of maximal-average indices of \(\eta\) up to \(m\) is the set of all \(i\) with \(1 \le i \le m\) such that \(A_j \le A_i\) for every \(j\) with \(1 \le j \le m\); for \(m \ge 1\) these are the \(i\) with \(1 \le i \le m\) and \(A_i = A_{\max}\), where \(A_{\max} = \max \{A_i \mid 1 \le i \le m\}\), and for \(m = 0\) the set is empty.

public noncomputable def maxAverageIndices (η : ℕ → ℕ) (m : ℕ) : Finset ℕ :=
  open scoped Classical in
  (Finset.Icc 1 m).filter fun i =>
    ∀ j ∈ Finset.Icc 1 m, binomidAverage η j ≤ binomidAverage η i

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Section 3 (the set {i ≤ m | A_max = A_i}).

Uses 1 · Used by 6

Statement usesInitial averages of a sequence

Used byThe largest of the first \(m\) averages is the largest average · A preperiod bound for lex-minimal extensions · Every index with maximal average is a multiple of the gcd of those up to \(m\) · The gcd of the maximizing indices divides the minimal period · Minimal period of a lex-minimal extension · Maximal-average indices for \(m = 1\)

TheoremMaximal-average indices for \(m = 1\)#✓fully proved

Let \(\eta = (e_1, e_2, \dots)\) be a sequence of nonnegative integers and \(A_i = (e_1 + \dots + e_i)/i\). For \(m = 1\), the set of indices \(1 \le i \le m\) at which \(A_i\) is maximal among \(A_1, \dots, A_m\) is \(\{1\}\).

public theorem maxAverageIndices_one (η : ℕ → ℕ) : maxAverageIndices η 1 = {1}

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Section 3.

Uses 2

Statement usesIndices of maximal average

Proof usesInitial averages of a sequence

DefinitionBasis of a submonoid#✓fully proved

Let \(M\) and \(B\) be subsets of an additive commutative monoid. Then \(B\) is a basis of \(M\) when \(M\) is the submonoid \(\langle B \rangle\) generated by \(B\) and no element of \(B\) is a nonnegative integer combination of elements of \(B\) in which its own coefficient is \(0\): for all pairwise distinct \(\beta_1, \dots, \beta_n \in B\), all nonnegative integers \(c_1, \dots, c_n\) and every \(j\), if \(\beta_j = \sum_{i=1}^n c_i \beta_i\) then \(c_j \ge 1\).

The elements \(\beta_i\) are required to be distinct: the paper's wording allows repeated entries, under which \(\beta = (b, b)\) and \(b = 0 \cdot b + 1 \cdot b\) would rule out every nonempty \(B\); its uniqueness proof uses distinct entries.

public def IsAddMonoidBasis {α : Type*} [AddCommMonoid α] (M B : Set α) : Prop :=
  (AddSubmonoid.closure B : Set α) = M ∧
    ∀ (n : ℕ) (β : Fin n → α), Function.Injective β → (∀ i, β i ∈ B) →
      ∀ (c : Fin n → ℕ) (j : Fin n), β j = ∑ i, c i • β i → 1 ≤ c j

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Section 4 (definition of a basis).

Used by 5

Used byBasis of the span of the lex-minimal extensions of length \(k\) · The empty set is a basis of the zero submonoid · Atoms are the unique basis of an atom-generated submonoid · Basis of the monoid of lex-minimal extensions · A monoid basis does not contain zero

TheoremA monoid basis does not contain zero#✓fully proved

Let \(\alpha\) be an additive commutative monoid and let \(M\) and \(B\) be subsets of \(\alpha\). If \(B\) is a basis of \(M\), then \(0 \notin B\).

public theorem IsAddMonoidBasis.zero_notMem {α : Type*} [AddCommMonoid α] {M B : Set α}
    (h : IsAddMonoidBasis M B) : (0 : α) ∉ B

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Section 4.

Uses 1

Statement usesBasis of a submonoid

TheoremThe empty set is a basis of the zero submonoid#✓fully proved

In every additive commutative monoid, the empty set is a basis of the subset \(\{0\}\).

public theorem isAddMonoidBasis_empty {α : Type*} [AddCommMonoid α] :
    IsAddMonoidBasis ({0} : Set α) ∅

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Section 4.

Uses 1

Statement usesBasis of a submonoid

DefinitionAtomic binomid index#✓fully proved

A sequence \(\eta\) of nonnegative integers is a nonzero atomic binomid index (an element of the paper's set \(\mathrm{Atom}\)) when \(\eta\) is a nonzero binomid index that is not the sum of two nonzero binomid indices: whenever \(\eta = \eta_1 + \eta_2\) termwise with \(\eta_1\) and \(\eta_2\) binomid indices, \(\eta_1 = 0\) or \(\eta_2 = 0\).

public def IsAtomicBinomidIndex (η : ℕ → ℕ) : Prop :=
  IsBinomidIndex η ∧ η ≠ 0 ∧
    ∀ η₁ η₂ : ℕ → ℕ, IsBinomidIndex η₁ → IsBinomidIndex η₂ → η = η₁ + η₂ →
      η₁ = 0 ∨ η₂ = 0

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Section 4 (definition of atomic).

Uses 1 · Used by 5

Statement usesBinomid index

Used bySpans of lex-minimal extensions of a fixed length are finitely generated · The monoid of lex-minimal extensions is a directed union · Basis of the span of the lex-minimal extensions of length \(k\) · Basis of the monoid of lex-minimal extensions · The constant sequence \(1\) is atomic

TheoremThe constant sequence \(1\) is atomic#✓fully proved

The constant sequence \((1, 1, 1, \dots)\) is a nonzero atomic binomid index: it is a nonzero binomid index that is not the sum of two nonzero binomid indices.

public theorem isAtomicBinomidIndex_one : IsAtomicBinomidIndex fun _ => 1

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Section 4 (example of (E_m)^∞ with m = 1).

Uses 3

Statement usesAtomic binomid index

Proof usesBinomid index · Constant sequences are binomid indices

TheoremPartial-sum criterion for lex-minimal extensions#●ready to prove

Let \(k \ge 1\), let \(\eta = (e_1, e_2, \dots)\) be a sequence of nonnegative integers and write \(S_i = e_1 + \dots + e_i\). Suppose \(S_i + S_j \le S_{i+j}\) for all \(i, j \ge 1\) with \(i + j \le k\). Then \(\eta\) is the lex-minimal extension of \((e_1, \dots, e_k)\) if and only if, for every \(r > k\), \(S_i + S_j \le S_r\) for all \(i, j \ge 1\) with \(i + j = r\), with equality for at least one such pair \((i, j)\).

In the paper's notation, the condition says that \(\Delta_\eta(r) = 0\) for every \(r > k\), where \(\Delta_\eta(r) = \min \{S_r - S_i - S_j : i + j = r,\ i, j \ge 1\}\).

public theorem_wanted isLexMinimalExtensionOf_iff_forall_lt {η : ℕ → ℕ} {k : ℕ}
    (hk : 1 ≤ k)
    (hpre : ∀ i j : ℕ, 1 ≤ i → 1 ≤ j → i + j ≤ k →
      ∑ l ∈ Finset.range i, η l + ∑ l ∈ Finset.range j, η l
        ≤ ∑ l ∈ Finset.range (i + j), η l) :
    IsLexMinimalExtensionOf η k ↔ ∀ r : ℕ, k < r →
      (∀ i j : ℕ, 1 ≤ i → 1 ≤ j → i + j = r →
        ∑ l ∈ Finset.range i, η l + ∑ l ∈ Finset.range j, η l
          ≤ ∑ l ∈ Finset.range r, η l) ∧
      ∃ i j : ℕ, 1 ≤ i ∧ 1 ≤ j ∧ i + j = r ∧
        ∑ l ∈ Finset.range i, η l + ∑ l ∈ Finset.range j, η l
          = ∑ l ∈ Finset.range r, η l

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Proposition 1.

Uses 1

Statement usesLex-minimal extension

TheoremPartial sums of a lex-minimal extension solve a knapsack problem#●ready to prove

Let \(m \ge 1\), let \(\eta = (e_1, e_2, \dots)\) be the lex-minimal extension of its first \(m\) entries, and write \(S_i = e_1 + \dots + e_i\). Then for every \(c \ge 1\) there are nonnegative integers \(n_1, \dots, n_m\) with \(\sum_{i=1}^m n_i i = c\) and \(S_c = \sum_{i=1}^m n_i S_i\) that solve the unbounded knapsack problem with values \(S_i\), weights \(i\) and capacity \(c\): all nonnegative integers \(n'_1, \dots, n'_m\) with \(\sum_{i=1}^m n'_i i \le c\) satisfy \(\sum_{i=1}^m n'_i S_i \le \sum_{i=1}^m n_i S_i\).

public theorem_wanted IsLexMinimalExtensionOf.exists_knapsack {η : ℕ → ℕ} {m : ℕ}
    (hη : IsLexMinimalExtensionOf η m) (hm : 1 ≤ m) {c : ℕ} (hc : 1 ≤ c) :
    ∃ n : ℕ → ℕ, ∑ i ∈ Finset.Icc 1 m, n i * i = c ∧
      ∑ l ∈ Finset.range c, η l
        = ∑ i ∈ Finset.Icc 1 m, n i * ∑ l ∈ Finset.range i, η l ∧
      ∀ n' : ℕ → ℕ, ∑ i ∈ Finset.Icc 1 m, n' i * i ≤ c →
        ∑ i ∈ Finset.Icc 1 m, n' i * ∑ l ∈ Finset.range i, η l
          ≤ ∑ i ∈ Finset.Icc 1 m, n i * ∑ l ∈ Finset.range i, η l

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Proposition 2.

Uses 1

Statement usesLex-minimal extension

TheoremThe largest of the first \(m\) averages is the largest average#●ready to prove

Let \(m \ge 0\) and let \(\eta = (e_1, e_2, \dots)\) be the lex-minimal extension of its first \(m\) entries, with averages \(A_i = (e_1 + \dots + e_i)/i\) for \(i \ge 1\). If \(1 \le j \le m\) and \(A_j = \max \{A_i \mid 1 \le i \le m\}\), then \(A_i \le A_j\) for every \(i \ge 1\).

public theorem_wanted IsLexMinimalExtensionOf.binomidAverage_le {η : ℕ → ℕ} {m : ℕ}
    (hη : IsLexMinimalExtensionOf η m) {i : ℕ} (hi : 1 ≤ i) {j : ℕ}
    (hj : j ∈ maxAverageIndices η m) :
    binomidAverage η i ≤ binomidAverage η j

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Lemma 1.

Uses 3

Statement usesLex-minimal extension · Initial averages of a sequence · Indices of maximal average

TheoremEvery index with maximal average is a multiple of the gcd of those up to \(m\)#●ready to prove

Let \(m \ge 0\), let \(\eta = (e_1, e_2, \dots)\) be the lex-minimal extension of its first \(m\) entries, with averages \(A_i = (e_1 + \dots + e_i)/i\), let \(J\) be the set of indices \(1 \le j \le m\) with \(A_j = \max \{A_{j'} \mid 1 \le j' \le m\}\), and let \(g = \gcd J\). Then \(g\) divides every \(i \ge 1\) such that \(A_i = A_j\) for some \(j \in J\).

Since every element of \(J\) is such an index, \(g\) is also the greatest common divisor of all \(i \ge 1\) with \(A_i = A_j\) for some \(j \in J\).

public theorem_wanted IsLexMinimalExtensionOf.gcd_maxAverageIndices_dvd {η : ℕ → ℕ}
    {m : ℕ} (hη : IsLexMinimalExtensionOf η m) {i : ℕ} (hi : 1 ≤ i)
    (hmax : ∃ j ∈ maxAverageIndices η m, binomidAverage η i = binomidAverage η j) :
    (maxAverageIndices η m).gcd id ∣ i

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Lemma 2.

Uses 3

Statement usesLex-minimal extension · Initial averages of a sequence · Indices of maximal average

TheoremThe gcd of the maximizing indices divides the minimal period#●ready to prove

Let \(m \ge 1\), let \(\eta = (e_1, e_2, \dots)\) be the lex-minimal extension of its first \(m\) entries, with averages \(A_i = (e_1 + \dots + e_i)/i\), and let \(g\) be the greatest common divisor of the indices \(1 \le i \le m\) with \(A_i = \max \{A_j \mid 1 \le j \le m\}\). If \(p\) is the least \(q \ge 1\) such that \(e_{i+q} = e_i\) for all sufficiently large \(i\), then \(g\) divides \(p\).

public theorem_wanted IsLexMinimalExtensionOf.gcd_maxAverageIndices_dvd_minimalPeriod
    {η : ℕ → ℕ} {m : ℕ} (hη : IsLexMinimalExtensionOf η m) (hm : 1 ≤ m) {p : ℕ}
    (hp : IsLeast {q : ℕ | 0 < q ∧ ∃ N, ∀ i, N ≤ i → η (i + q) = η i} p) :
    (maxAverageIndices η m).gcd id ∣ p

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Lemma 3.

Uses 2

Statement usesLex-minimal extension · Indices of maximal average

TheoremMinimal period of a lex-minimal extension#●ready to prove

Let \(m \ge 1\) and let \(\eta = (e_1, e_2, \dots)\) be the lex-minimal extension of \((e_1, \dots, e_m)\). For \(1 \le i \le m\) let \(A_i = (e_1 + \dots + e_i)/i\), and let \(A_{\max}\) be the largest of \(A_1, \dots, A_m\). Let \(g\) be the greatest common divisor of the indices \(1 \le i \le m\) with \(A_i = A_{\max}\). Then \(g\) is the minimal eventual period of \(\eta\): \(g \ge 1\), \(e_{i+g} = e_i\) for all sufficiently large \(i\), and every \(q \ge 1\) with \(e_{i+q} = e_i\) for all sufficiently large \(i\) satisfies \(g \le q\).

public theorem_wanted IsLexMinimalExtensionOf.isLeast_period_gcd_maxAverageIndices
    {η : ℕ → ℕ} {m : ℕ} (hη : IsLexMinimalExtensionOf η m) (hm : 1 ≤ m) :
    IsLeast {q : ℕ | 0 < q ∧ ∃ N, ∀ i, N ≤ i → η (i + q) = η i}
      ((maxAverageIndices η m).gcd id)

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Theorem 1.

Uses 2

Statement usesLex-minimal extension · Indices of maximal average

TheoremA preperiod bound for lex-minimal extensions#●ready to prove

Let \(m \ge 0\), let \(\eta = (e_1, e_2, \dots)\) be the lex-minimal extension of its first \(m\) entries, with averages \(A_i = (e_1 + \dots + e_i)/i\), and let \(1 \le k \le m\) with \(A_k = \max \{A_i \mid 1 \le i \le m\}\). Then \(\eta\) is periodic after position \(N = k m (m + 1)/2\): there is \(p \ge 1\) with \(e_{i+p} = e_i\) for all \(i > N\).

public theorem_wanted IsLexMinimalExtensionOf.exists_period_from_preperiod_bound
    {η : ℕ → ℕ} {m : ℕ} (hη : IsLexMinimalExtensionOf η m) {k : ℕ}
    (hk : k ∈ maxAverageIndices η m) :
    ∃ p, 0 < p ∧ ∀ j, k * (m * (m + 1) / 2) ≤ j → η (j + p) = η j

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Theorem 2.

Uses 2

Statement usesLex-minimal extension · Indices of maximal average

TheoremSummands of a lex-minimal extension are lex-minimal#●ready to prove

Let \(\eta_1\) and \(\eta_2\) be infinite binomid indices and let \(k \ge 0\). If the termwise sum \(\eta_1 + \eta_2\) is the lex-minimal extension of its first \(k\) entries, then \(\eta_1\) is the lex-minimal extension of its first \(k\) entries and \(\eta_2\) is the lex-minimal extension of its first \(k\) entries.

Since every lex-minimal extension is the lex-minimal extension of its first \(k\) entries for some \(k\), this contains the first claim of the source: if \(\eta_1 + \eta_2\) is a lex-minimal extension, then so are \(\eta_1\) and \(\eta_2\).

public theorem_wanted IsLexMinimalExtensionOf.of_add {η₁ η₂ : ℕ → ℕ} {k : ℕ}
    (h : IsLexMinimalExtensionOf (η₁ + η₂) k) (h₁ : IsBinomidIndex η₁)
    (h₂ : IsBinomidIndex η₂) :
    IsLexMinimalExtensionOf η₁ k ∧ IsLexMinimalExtensionOf η₂ k

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Proposition 3.

Uses 2

Statement usesBinomid index · Lex-minimal extension

TheoremAtoms are the unique basis of an atom-generated submonoid#●ready to prove

Let \(\iota\) be a type and let \(M\) be a submonoid of \(\mathbb{N}^\iota\) under componentwise addition. Let \(A\) be the set of atoms of \(M\): the elements \(a \in M\) with \(a \ne 0\) such that \(y = 0\) or \(z = 0\) whenever \(a = y + z\) with \(y, z \in M\). If every element of \(M\) is a finite sum of elements of \(A\), then a set \(B \subseteq \mathbb{N}^\iota\) is a basis of \(M\) if and only if \(B = A\); that is, \(A\) is the unique basis of \(M\).

public theorem_wanted isAddMonoidBasis_iff_eq_atoms {ι : Type*} (M : AddSubmonoid (ι → ℕ))
    (hM : ∀ x ∈ M, x ∈ AddSubmonoid.closure
      {a | a ∈ M ∧ a ≠ 0 ∧ ∀ y ∈ M, ∀ z ∈ M, a = y + z → y = 0 ∨ z = 0})
    (B : Set (ι → ℕ)) :
    IsAddMonoidBasis (M : Set (ι → ℕ)) B ↔
      B = {a | a ∈ M ∧ a ≠ 0 ∧ ∀ y ∈ M, ∀ z ∈ M, a = y + z → y = 0 ∨ z = 0}

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Proposition 4.

Uses 1

Statement usesBasis of a submonoid

TheoremBasis of the monoid of lex-minimal extensions#●ready to prove

Let \(L\) be the set of lex-minimal extensions, viewed inside the sequences of nonnegative integers under componentwise addition. A set \(B\) of sequences of nonnegative integers is a basis of \(L\) if and only if \(B\) is the set of nonzero atomic binomid indices that belong to \(L\). Hence that set is the unique basis of \(L\).

public theorem_wanted isAddMonoidBasis_lexMinimalExtensions_iff (B : Set (ℕ → ℕ)) :
    IsAddMonoidBasis {η | IsLexMinimalExtension η} B ↔
      B = {η | IsAtomicBinomidIndex η ∧ IsLexMinimalExtension η}

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Proposition 5.

Uses 3

Statement usesBasis of a submonoid · Atomic binomid index · Lex-minimal extensions

TheoremBasis of the span of the lex-minimal extensions of length \(k\)#●ready to prove

Let \(k \ge 0\) and let \(L_k\) be the set of sequences \(\eta = (e_1, e_2, \dots)\) of nonnegative integers that are the lex-minimal extension of \((e_1, \dots, e_k)\). A set \(B\) of sequences of nonnegative integers is a basis of the submonoid generated by \(L_k\) under componentwise addition if and only if \(B\) is the set of nonzero atomic binomid indices that belong to \(L_k\). Hence that set is the unique basis of this submonoid.

public theorem_wanted isAddMonoidBasis_closure_lexMinimalExtensionsOf_iff (k : ℕ)
    (B : Set (ℕ → ℕ)) :
    IsAddMonoidBasis
        (AddSubmonoid.closure {η : ℕ → ℕ | IsLexMinimalExtensionOf η k} : Set (ℕ → ℕ)) B ↔
      B = {η | IsAtomicBinomidIndex η ∧ IsLexMinimalExtensionOf η k}

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Proposition 5.

Uses 3

Statement usesBasis of a submonoid · Atomic binomid index · Lex-minimal extension

TheoremLate partial sums of a lex-minimal extension split#●ready to prove

Let \(k \ge 1\), let \(\eta = (e_1, e_2, \dots)\) be the lex-minimal extension of its first \(k\) entries, and write \(S_i = e_1 + \dots + e_i\). Then for every \(l\) there is a map \(\pi \colon \mathbb{N} \to \mathbb{N}\) such that \(1 \le \pi(i) < i\) and \(S_i = S_{\pi(i)} + S_{i - \pi(i)}\) for every \(i\) with \(k < i \le l\).

The paper takes the specific bound \(l = l(k)\) from its proof of the preceding lemma; the statement here holds for every \(l\).

public theorem_wanted IsLexMinimalExtensionOf.exists_path {η : ℕ → ℕ} {k : ℕ}
    (hη : IsLexMinimalExtensionOf η k) (hk : 1 ≤ k) (l : ℕ) :
    ∃ π : ℕ → ℕ, ∀ i, k < i → i ≤ l → 1 ≤ π i ∧ π i < i ∧
      ∑ t ∈ Finset.range i, η t
        = ∑ t ∈ Finset.range (π i), η t + ∑ t ∈ Finset.range (i - π i), η t

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Lemma 4.

Uses 1

Statement usesLex-minimal extension

TheoremSpans of lex-minimal extensions of a fixed length are finitely generated#●ready to prove

For \(k \ge 0\) let \(L_k\) be the set of sequences of nonnegative integers that are the lex-minimal extension of their first \(k\) entries. Then the submonoid of \(\mathbb{N}^{\mathbb{N}}\) (under componentwise addition) generated by \(L_k\) is finitely generated, and only finitely many elements of \(L_k\) are atomic binomid indices, that is, nonzero binomid indices that are not the sum of two nonzero binomid indices.

public theorem_wanted fg_closure_lexMinimalExtensionsOf (k : ℕ) :
    (AddSubmonoid.closure {η : ℕ → ℕ | IsLexMinimalExtensionOf η k}).FG ∧
      {η | IsAtomicBinomidIndex η ∧ IsLexMinimalExtensionOf η k}.Finite

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Lemma 5.

Uses 2

Statement usesAtomic binomid index · Lex-minimal extension

TheoremSpans of lex-minimal extensions of a fixed length are finitely presented#●ready to prove

For \(k \ge 0\) let \(L_k\) be the set of sequences of nonnegative integers that are the lex-minimal extension of their first \(k\) entries, and let \(\langle L_k \rangle\) be the submonoid of \(\mathbb{N}^{\mathbb{N}}\) (under componentwise addition) generated by \(L_k\). Then there are \(n \ge 0\), a surjective monoid homomorphism \(f \colon \mathbb{N}^n \to \langle L_k \rangle\) and a finite set \(R\) of pairs of elements of \(\mathbb{N}^n\) such that the congruence on \(\mathbb{N}^n\) generated by \(R\) is the kernel congruence of \(f\), which relates \(x\) and \(y\) exactly when \(f(x) = f(y)\).

public theorem_wanted exists_finitePresentation_closure_lexMinimalExtensionsOf (k : ℕ) :
    ∃ (n : ℕ) (f : (Fin n → ℕ) →+
        AddSubmonoid.closure {η : ℕ → ℕ | IsLexMinimalExtensionOf η k}),
      Function.Surjective f ∧ ∃ R : Set ((Fin n → ℕ) × (Fin n → ℕ)), R.Finite ∧
        addConGen (fun x y => (x, y) ∈ R) = AddCon.ker f

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Lemma 6.

Uses 1

Statement usesLex-minimal extension

TheoremThe monoid of lex-minimal extensions is a directed union#●ready to prove

For \(k \ge 0\) let \(L_k\) be the set of sequences of nonnegative integers that are the lex-minimal extension of their first \(k\) entries, let \(\langle L_k \rangle\) be the submonoid of \(\mathbb{N}^{\mathbb{N}}\) (under componentwise addition) generated by \(L_k\), and let \(\mathcal{A}_k\) be the set of elements of \(L_k\) that are atomic binomid indices, that is, nonzero binomid indices that are not the sum of two nonzero binomid indices. Then \(\langle L_k \rangle \subseteq \langle L_{k'} \rangle\) and \(\mathcal{A}_k \subseteq \mathcal{A}_{k'}\) whenever \(k \le k'\); the union of the sets \(\langle L_k \rangle\) over all \(k\) is the set \(L\) of all lex-minimal extensions; and for every \(k\) the submonoid generated by \(\mathcal{A}_k\) is \(\langle L_k \rangle\).

public theorem_wanted iUnion_closure_lexMinimalExtensionsOf :
    Monotone (fun k => AddSubmonoid.closure {η : ℕ → ℕ | IsLexMinimalExtensionOf η k}) ∧
    (⋃ k, (AddSubmonoid.closure {η : ℕ → ℕ | IsLexMinimalExtensionOf η k} :
        Set (ℕ → ℕ))) = {η | IsLexMinimalExtension η} ∧
    Monotone (fun k => {η : ℕ → ℕ | IsAtomicBinomidIndex η ∧ IsLexMinimalExtensionOf η k}) ∧
    ∀ k, AddSubmonoid.closure {η : ℕ → ℕ | IsAtomicBinomidIndex η ∧ IsLexMinimalExtensionOf η k}
      = AddSubmonoid.closure {η : ℕ → ℕ | IsLexMinimalExtensionOf η k}

Sources

• Caalim and Tanaka, Generalized Binomial Coefficients and the Monoid of Lexicographically Minimal Extensions, INTEGERS 26 (2026), Article A113, Theorem 3.

Uses 3

Statement usesAtomic binomid index · Lex-minimal extensions · Lex-minimal extension

21 fully proved31 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.