Weighted zero-sum free sequences to Weighted zero-sum subsequences are monotone in the weight set

DefinitionWeighted zero-sum free sequences#✓fully proved

Let \(G\) be an additive commutative monoid and \(A\) a finite set of natural numbers. A finite sequence \(s = (s_1, \dots, s_n)\) over \(G\) is \(A\)-weighted zero-sum free when, for every non-empty set \(I \subseteq \{1, \dots, n\}\) of positions and every choice of weights \(a_i \in A\) for \(i \in I\), the weighted sum \(\sum_{i \in I} a_i s_i\) is non-zero, where \(a_i s_i\) is the sum of \(a_i\) copies of \(s_i\). Terms are indexed by position, so repeated terms count separately.

def IsWeightedZeroSumFree {G : Type*} [AddCommMonoid G] (A : Finset ℕ) (s : List G) :
    Prop :=
  ∀ I : Finset (Fin s.length), I.Nonempty → ∀ a : Fin s.length → ℕ,
    (∀ i ∈ I, a i ∈ A) → ∑ i ∈ I, a i • s.get i ≠ 0
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Section 2 (weighted zero-sum subsequences, as used in Lemmas 2 and 3).
Used by 10
Used byLower bound for the weighted Davenport constant · Prefixes of weighted zero-sum free sequences · Weighted Davenport constant · The weighted Davenport constant as a least length · When the weighted Davenport constant is infinite · Upper bound for the weighted Davenport constant · Davenport constant of the group of order two · Weighted Davenport constant of the trivial group · Long weighted zero-sum free sequences in abelian \(p\)-groups · Long weighted zero-sum free sequences in groups of rank two

DefinitionWeighted Davenport constant#✓fully proved

Let \(G\) be an additive commutative monoid and \(A\) a finite set of natural numbers. The \(A\)-weighted Davenport constant \(D_A(G) \in \mathbb{N} \cup \{\infty\}\) is the least length \(\ell \in \mathbb{N}\) such that no sequence over \(G\) of length \(\ell\) is \(A\)-weighted zero-sum free, that is, such that every sequence over \(G\) of length \(\ell\) has a non-empty \(A\)-weighted zero-sum subsequence; it is \(\infty\) when no such length exists.

For example \(D_A(G) = \infty\) when \(A = \emptyset\), or when \(A = \{1\}\) and \(G = \mathbb{Z}\). For a finite group \(G\) and a non-empty weight set \(A\) it is finite. The ordinary Davenport constant of \(G\) is \(D_{\{1\}}(G)\).

noncomputable def weightedDavenport (A : Finset ℕ) (G : Type*) [AddCommMonoid G] : ℕ∞ :=
  ⨅ ℓ ∈ {ℓ : ℕ | ∀ s : List G, s.length = ℓ → ¬ IsWeightedZeroSumFree A s}, (ℓ : ℕ∞)
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Section 2 (definition of D_A(G)).
Uses 1 · Used by 29
Statement usesWeighted zero-sum free sequences
Used byLower bound for the weighted Davenport constant · The weighted Davenport constant as a least length · When the weighted Davenport constant is infinite · Upper bound for the weighted Davenport constant · Davenport constant of the group of order two · Weighted Davenport constant of the trivial group · Square-weighted constants of even squares · Square-weighted constants modulo \(p^r\), for \(p \ge 2\) and nonzero even \(r\), are at most unit-square constants modulo \(p^2\) · Square-weighted constants of nonsquares with even \(2\)-adic valuation · Square-weighted Davenport constant of even squares is at least four · Square-weighted Davenport constant for an even 2-adic valuation of at least two · The square-weighted Davenport constant of an odd modulus is at least three · Square-weighted constants of numbers with odd \(2\)-adic valuation · Olson's theorem for abelian \(p\)-groups · Olson's theorem for groups of rank at most two · The square-weighted Davenport constant of an even power of an odd prime is at most five · The square-weighted Davenport constant of an odd square is at least five · The square-weighted Davenport constant of an odd square is five · Xia's theorem on arithmetic progressions of weights · Weighted Davenport constant of \(\mathbb{Z}/n\mathbb{Z}\) for the weights prime to \(p\) · Weighted Davenport constant of \((\mathbb{Z}/p^e\mathbb{Z})^r\) · Weighted Davenport constant of abelian \(p\)-groups, divisible case · Weighted Davenport constant of abelian \(p\)-groups, non-divisible case · Weighted Davenport constant of \(\mathbb{Z}/n\mathbb{Z}\) for the weights \(\{1, \dots, r\}\) · Initial-interval weights with weighted Davenport constant \(m\) · Weight sets with weighted Davenport constant \(m\) on \(\mathbb{Z}/n\mathbb{Z}\) · Weight sets with prescribed weighted Davenport constant on \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/kn\mathbb{Z}\), divisible case · Weight sets with prescribed weighted Davenport constant on \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/kn\mathbb{Z}\), non-divisible case · Weight sets with weighted Davenport constant \(2m - 1\) on \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z}\)

TheoremThe weighted Davenport constant as a least length#✓fully proved

Let \(G\) be an additive commutative monoid, \(A\) a finite set of natural numbers and \(D_A(G)\) the \(A\)-weighted Davenport constant of \(G\). If there is a length \(\ell \in \mathbb{N}\) such that no sequence over \(G\) of length \(\ell\) is \(A\)-weighted zero-sum free, then \(D_A(G)\) is finite and equals the least such length.

theorem weightedDavenport_eq_natCast_sInf (A : Finset ℕ) (G : Type*) [AddCommMonoid G]
    (h : {ℓ : ℕ | ∀ s : List G, s.length = ℓ → ¬ IsWeightedZeroSumFree A s}.Nonempty) :
    weightedDavenport A G =
      ((sInf {ℓ : ℕ | ∀ s : List G, s.length = ℓ → ¬ IsWeightedZeroSumFree A s} : ℕ) : ℕ∞)
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Section 2 (definition of D_A(G)).
Uses 2 · Used by 3
Statement usesWeighted zero-sum free sequences · Weighted Davenport constant
Used byLower bound for the weighted Davenport constant · Davenport constant of the group of order two · Weighted Davenport constant of the trivial group

TheoremPrefixes of weighted zero-sum free sequences#✓fully proved

Let \(G\) be an additive commutative monoid and \(A\) a finite set of natural numbers. If a sequence \(s\) over \(G\) is \(A\)-weighted zero-sum free, then for every \(\ell \in \mathbb{N}\) the prefix of \(s\) formed by its first \(\ell\) terms (all of \(s\) when \(\ell\) is at least its length) is \(A\)-weighted zero-sum free.

theorem IsWeightedZeroSumFree.take {G : Type*} [AddCommMonoid G] {A : Finset ℕ}
    {s : List G} (hs : IsWeightedZeroSumFree A s) (ℓ : ℕ) :
    IsWeightedZeroSumFree A (s.take ℓ)
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Section 2 (definition of D_A(G)).
Uses 1 · Used by 1
Statement usesWeighted zero-sum free sequences
Used byLower bound for the weighted Davenport constant

TheoremUpper bound for the weighted Davenport constant#✓fully proved

Let \(G\) be an additive commutative monoid, \(A\) a finite set of natural numbers, \(D_A(G)\) the \(A\)-weighted Davenport constant of \(G\) and \(\ell\) a natural number. If no sequence over \(G\) of length \(\ell\) is \(A\)-weighted zero-sum free, that is, every sequence over \(G\) of length \(\ell\) has a non-empty \(A\)-weighted zero-sum subsequence, then \(D_A(G) \le \ell\).

theorem weightedDavenport_le {G : Type*} [AddCommMonoid G] {A : Finset ℕ} {ℓ : ℕ}
    (h : ∀ s : List G, s.length = ℓ → ¬ IsWeightedZeroSumFree A s) :
    weightedDavenport A G ≤ ℓ
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Section 2 (definition of D_A(G)).
Uses 2
Statement usesWeighted zero-sum free sequences · Weighted Davenport constant

TheoremLower bound for the weighted Davenport constant#✓fully proved

Let \(G\) be an additive commutative monoid, \(A\) a finite set of natural numbers and \(D_A(G)\) the \(A\)-weighted Davenport constant of \(G\). If a sequence over \(G\) of length \(L\) is \(A\)-weighted zero-sum free, then \(L < D_A(G)\).

theorem lt_weightedDavenport {G : Type*} [AddCommMonoid G] {A : Finset ℕ} {s : List G}
    (hs : IsWeightedZeroSumFree A s) : (s.length : ℕ∞) < weightedDavenport A G
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Section 2 (definition of D_A(G)).
Uses 4
Statement usesWeighted zero-sum free sequences · Weighted Davenport constant
Proof usesPrefixes of weighted zero-sum free sequences · The weighted Davenport constant as a least length

TheoremWhen the weighted Davenport constant is infinite#✓fully proved

Let \(G\) be an additive commutative monoid, \(A\) a finite set of natural numbers and \(D_A(G)\) the \(A\)-weighted Davenport constant of \(G\). Then \(D_A(G) = \infty\) if and only if for every \(\ell \in \mathbb{N}\) there is an \(A\)-weighted zero-sum free sequence over \(G\) of length \(\ell\).

theorem weightedDavenport_eq_top_iff {G : Type*} [AddCommMonoid G] {A : Finset ℕ} :
    weightedDavenport A G = ⊤ ↔
      ∀ ℓ : ℕ, ∃ s : List G, s.length = ℓ ∧ IsWeightedZeroSumFree A s
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Section 2 (definition of D_A(G)).
Uses 2
Statement usesWeighted zero-sum free sequences · Weighted Davenport constant

TheoremWeighted Davenport constant of the trivial group#✓fully proved

For every non-empty finite set \(A\) of natural numbers, the \(A\)-weighted Davenport constant of the trivial group \(\mathbb{Z}/1\mathbb{Z}\) is \(D_A(\mathbb{Z}/1\mathbb{Z}) = 1\).

theorem weightedDavenport_zmod_one (A : Finset ℕ) (hA : A.Nonempty) :
    weightedDavenport A (ZMod 1) = 1
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Section 2 (characteristic value of D_A).
Uses 3
Statement usesWeighted Davenport constant
Proof usesWeighted zero-sum free sequences · The weighted Davenport constant as a least length

TheoremDavenport constant of the group of order two#✓fully proved

The ordinary Davenport constant of \(\mathbb{Z}/2\mathbb{Z}\), that is, its \(\{1\}\)-weighted Davenport constant, is \(D_{\{1\}}(\mathbb{Z}/2\mathbb{Z}) = 2\).

theorem weightedDavenport_singleton_one_zmod_two :
    weightedDavenport {1} (ZMod 2) = 2
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Section 2 (characteristic value of D_A).
Uses 3
Statement usesWeighted Davenport constant
Proof usesWeighted zero-sum free sequences · The weighted Davenport constant as a least length

DefinitionUnits modulo n#✓fully proved

For a natural number \(n\), \(U(n)\) is the set of units of the ring \(\mathbb{Z}/n\mathbb{Z}\) of integers modulo \(n\).

public def unitSet (n : ℕ) : Set (ZMod n) := {x | IsUnit x}
Sources
  • Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Introduction.

DefinitionSquares of units modulo n#✓fully proved

For a natural number \(n\), \(U(n)^2\) is the set of elements of \(\mathbb{Z}/n\mathbb{Z}\) of the form \(u^2\) with \(u\) a unit of \(\mathbb{Z}/n\mathbb{Z}\).

public def unitSquareSet (n : ℕ) : Set (ZMod n) := {x | ∃ u, IsUnit u ∧ x = u ^ 2}
Sources
  • Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Introduction.
Used by 8
Used byScaled unit squares modulo a prime power · Number of nonzero squares modulo a prime power · Square-weighted constants modulo \(p^r\), for \(p \ge 2\) and nonzero even \(r\), are at most unit-square constants modulo \(p^2\) · Decomposition of the nonzero squares modulo a prime power · Lifting weighted zero sums from p² to an even power of p · Three unit-square cosets sum to every residue modulo an odd prime power · Four unit terms force a unit-square-weighted zero sum modulo a power of 5 · Unit-square-weighted consecutive constant modulo 25 equals nine

DefinitionNonzero squares modulo \(n\)#✓fully proved

For a natural number \(n\), \(S(n)\) is the set of elements \(x\) of \(\mathbb{Z}_n = \mathbb{Z}/n\mathbb{Z}\) with \(x \neq 0\) and \(x = y^2\) for some \(y \in \mathbb{Z}_n\).

public def squareSet (n : ℕ) : Set (ZMod n) := {x | x ≠ 0 ∧ ∃ y, x = y ^ 2}
Sources
  • Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Introduction.
Used by 31
Used byTwo units without square-weighted zero sums modulo any prime divisor · Number of nonzero squares modulo a prime power · Three-term sequences without square-weighted zero-sum subsequences · Square-weighted zero-sum free unit pairs lift to odd prime powers · Square-weighted zero-sum free unit triples modulo even powers of two · Square-weighted constants of even squares · Square-weighted constants modulo \(p^r\), for \(p \ge 2\) and nonzero even \(r\), are at most unit-square constants modulo \(p^2\) · Square-weighted constants of nonsquares with even \(2\)-adic valuation · Decomposition of the nonzero squares modulo a prime power · Square-weighted zero sums lift from a prime-power component · Square-weighted zero sums lift from \(p\) to odd powers \(p^r\) · Lifting weighted zero sums from p² to an even power of p · Prime-power bound for the square-weighted consecutive constant · Consecutive square-weighted constant of an even power of two is at most four · Consecutive square-weighted constant of an odd prime to an odd power is at most three · Square-weighted Davenport constant of even squares is at least four · Square-weighted Davenport constant for an even 2-adic valuation of at least two · The square-weighted Davenport constant of an odd modulus is at least three · The one-term zero sequence has a square-weighted zero sum · Four-term sequences without square-weighted zero-sum subsequences · Square-weighted constants of numbers with odd \(2\)-adic valuation · Consecutive square-weighted constant of an odd power of two is at most two · Consecutive square-weighted constant of an odd square is at most nine · Square-weighted consecutive constant of \(p^r\) for prime \(p \ge 7\) and even \(r \ge 4\) is at most five · Square-weighted consecutive constant five for odd squares with a large prime fourth power · Square-weighted consecutive constant of \(5^r\) for even \(r \ge 4\) is at most seven · Square-weighted consecutive constant of squares divisible by 625 is at most seven · Consecutive square-weighted constant of the square of an odd squarefree number · The square-weighted Davenport constant of an even power of an odd prime is at most five · The square-weighted Davenport constant of an odd square is at least five · The square-weighted Davenport constant of an odd square is five

DefinitionWeighted zero-sum sequences#✓fully proved

Let \(A \subseteq \mathbb{Z}/n\mathbb{Z}\) and let \(S = (x_1, \dots, x_k)\) be a sequence in \(\mathbb{Z}/n\mathbb{Z}\). Then \(S\) is an \(A\)-weighted zero-sum sequence if there are weights \(a_1, \dots, a_k \in A\) with \(a_1 x_1 + a_2 x_2 + \dots + a_k x_k = 0\).

public def HasWeightedZeroSum {n k : ℕ} (A : Set (ZMod n)) (S : Fin k → ZMod n) : Prop :=
  ∃ a : Fin k → ZMod n, (∀ i, a i ∈ A) ∧ ∑ i, a i * S i = 0
Sources
  • Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Introduction.
Used by 6
Used byThree-term sequences without square-weighted zero-sum subsequences · Square-weighted zero sums lift from a prime-power component · Square-weighted zero sums lift from \(p\) to odd powers \(p^r\) · Lifting weighted zero sums from p² to an even power of p · The one-term zero sequence has a square-weighted zero sum · Four unit terms force a unit-square-weighted zero sum modulo a power of 5

DefinitionWeighted zero-sum subsequences#✓fully proved

Let \(A \subseteq \mathbb{Z}/n\mathbb{Z}\) and let \(S = (x_1, \dots, x_k)\) be a sequence in \(\mathbb{Z}/n\mathbb{Z}\). Then \(S\) has an \(A\)-weighted zero-sum subsequence if there are a nonempty set \(J \subseteq \{1, \dots, k\}\) of indices and weights \(a_i \in A\) for \(i \in J\) with \(\sum_{i \in J} a_i x_i = 0\).

public def HasWeightedZeroSumSubseq {n k : ℕ} (A : Set (ZMod n))
    (S : Fin k → ZMod n) : Prop :=
  ∃ J : Finset (Fin k), J.Nonempty ∧
    ∃ a : Fin k → ZMod n, (∀ i ∈ J, a i ∈ A) ∧ ∑ i ∈ J, a i * S i = 0
Sources
  • Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Introduction.
Used by 6
Used byWeighted zero-sum subsequences are monotone in the weight set · Two units without square-weighted zero sums modulo any prime divisor · Three-term sequences without square-weighted zero-sum subsequences · Square-weighted zero-sum free unit pairs lift to odd prime powers · Square-weighted zero-sum free unit triples modulo even powers of two · Four-term sequences without square-weighted zero-sum subsequences

DefinitionConsecutive weighted zero-sum subsequences#✓fully proved

Let \(A \subseteq \mathbb{Z}/n\mathbb{Z}\) and let \(S = (x_1, \dots, x_k)\) be a sequence in \(\mathbb{Z}/n\mathbb{Z}\). Then \(S\) has an \(A\)-weighted zero-sum consecutive subsequence if there are indices \(1 \le l \le h \le k\) and weights \(a_l, \dots, a_h \in A\) with \(\sum_{i=l}^{h} a_i x_i = 0\).

public def HasConsecutiveWeightedZeroSumSubseq {n k : ℕ} (A : Set (ZMod n))
    (S : Fin k → ZMod n) : Prop :=
  ∃ J : Finset (Fin k), J.Nonempty ∧
    (∃ lo hi : ℕ, J = Finset.univ.filter fun i => lo ≤ i.1 ∧ i.1 ≤ hi) ∧
    ∃ a : Fin k → ZMod n, (∀ i ∈ J, a i ∈ A) ∧ ∑ i ∈ J, a i * S i = 0
Sources
  • Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Introduction.
Used by 1
Used byLengths forcing a consecutive weighted zero sum

DefinitionRepresentatives of a set of residues#✓fully proved

Let \(n\) be a natural number and \(A\) a subset of \(\mathbb{Z}_n\). The representatives of \(A\) form the finite set of natural numbers \(a\) with \(0 \le a < n\) whose residue modulo \(n\) lies in \(A\).

A natural number \(a\) acts on \(\mathbb{Z}_n\) by \(x \mapsto a x\). For \(n \ge 1\) every residue has exactly one representative below \(n\), so the weighted Davenport constant of \(\mathbb{Z}_n\) with the representatives of \(A\) as weights is the paper's \(D_A\).

public noncomputable def zmodWeightReps {n : ℕ} (A : Set (ZMod n)) : Finset ℕ :=
  open Classical in (Finset.range n).filter fun a => (a : ZMod n) ∈ A
Sources
  • Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Introduction.
Used by 11
Used byMembership in the weight representatives · Square-weighted constants of even squares · Square-weighted constants modulo \(p^r\), for \(p \ge 2\) and nonzero even \(r\), are at most unit-square constants modulo \(p^2\) · Square-weighted constants of nonsquares with even \(2\)-adic valuation · Square-weighted Davenport constant of even squares is at least four · Square-weighted Davenport constant for an even 2-adic valuation of at least two · The square-weighted Davenport constant of an odd modulus is at least three · Square-weighted constants of numbers with odd \(2\)-adic valuation · The square-weighted Davenport constant of an even power of an odd prime is at most five · The square-weighted Davenport constant of an odd square is at least five · The square-weighted Davenport constant of an odd square is five

TheoremMembership in the weight representatives#✓fully proved

Let \(A \subseteq \mathbb{Z}/n\mathbb{Z}\). A natural number \(a\) lies in the set of weight representatives of \(A\) if and only if \(a < n\) and the residue of \(a\) modulo \(n\) lies in \(A\).

public theorem mem_zmodWeightReps {n : ℕ} {A : Set (ZMod n)} {a : ℕ} :
    a ∈ zmodWeightReps A ↔ a < n ∧ (a : ZMod n) ∈ A
Sources
  • Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Introduction.
Uses 1
Statement usesRepresentatives of a set of residues

DefinitionLengths forcing a consecutive weighted zero sum#✓fully proved

Let \(n\) be a natural number and \(A\) a subset of \(\mathbb{Z}_n = \mathbb{Z}/n\mathbb{Z}\). This is the set of positive integers \(k\) such that every sequence \((x_1, \dots, x_k)\) of elements of \(\mathbb{Z}_n\) has a nonempty block of consecutive terms \(x_i, \dots, x_j\) with weights \(a_i, \dots, a_j \in A\) such that \(a_i x_i + \dots + a_j x_j = 0\). Its least element, or \(0\) when it is empty, is the \(A\)-weighted consecutive constant \(C_A\) of \(\mathbb{Z}_n\).

public def weightedConsecutiveDefiningSet (n : ℕ) (A : Set (ZMod n)) : Set ℕ :=
  {k | 0 < k ∧ ∀ S : Fin k → ZMod n, HasConsecutiveWeightedZeroSumSubseq A S}
Sources
  • Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Introduction.
Uses 1 · Used by 7
Statement usesConsecutive weighted zero-sum subsequences
Used byWeighted consecutive zero-sum constant · Square-weighted constants of even squares · Square-weighted constants of nonsquares with even \(2\)-adic valuation · Square-weighted constants of numbers with odd \(2\)-adic valuation · Square-weighted consecutive constant five for odd squares with a large prime fourth power · Consecutive square-weighted constant of the square of an odd squarefree number · Unit-square-weighted consecutive constant modulo 25 equals nine

DefinitionWeighted consecutive zero-sum constant#✓fully proved

Let \(n\) be a natural number and \(A\) a subset of \(\mathbb{Z}_n = \mathbb{Z}/n\mathbb{Z}\). The \(A\)-weighted consecutive constant \(C_A\) of \(\mathbb{Z}_n\) is the least positive integer \(k\) such that every sequence \((x_1, \dots, x_k)\) of elements of \(\mathbb{Z}_n\) has a nonempty block of consecutive terms \(x_i, \dots, x_j\) with weights \(a_i, \dots, a_j \in A\) such that \(a_i x_i + \dots + a_j x_j = 0\); it is \(0\) when no such \(k\) exists.

public noncomputable def weightedConsecutiveConstant (n : ℕ) (A : Set (ZMod n)) : ℕ :=
  sInf (weightedConsecutiveDefiningSet n A)
Sources
  • Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Introduction.
Uses 1 · Used by 15
Statement usesLengths forcing a consecutive weighted zero sum
Used bySquare-weighted constants of even squares · Square-weighted constants modulo \(p^r\), for \(p \ge 2\) and nonzero even \(r\), are at most unit-square constants modulo \(p^2\) · Square-weighted constants of nonsquares with even \(2\)-adic valuation · Prime-power bound for the square-weighted consecutive constant · Consecutive square-weighted constant of an even power of two is at most four · Consecutive square-weighted constant of an odd prime to an odd power is at most three · Square-weighted constants of numbers with odd \(2\)-adic valuation · Consecutive square-weighted constant of an odd power of two is at most two · Consecutive square-weighted constant of an odd square is at most nine · Square-weighted consecutive constant of \(p^r\) for prime \(p \ge 7\) and even \(r \ge 4\) is at most five · Square-weighted consecutive constant five for odd squares with a large prime fourth power · Square-weighted consecutive constant of \(5^r\) for even \(r \ge 4\) is at most seven · Square-weighted consecutive constant of squares divisible by 625 is at most seven · Consecutive square-weighted constant of the square of an odd squarefree number · Unit-square-weighted consecutive constant modulo 25 equals nine

TheoremWeighted zero-sum subsequences are monotone in the weight set#✓fully proved

Let \(A \subseteq B \subseteq \mathbb{Z}/n\mathbb{Z}\) and let \(S\) be a finite sequence in \(\mathbb{Z}/n\mathbb{Z}\). If \(S\) has an \(A\)-weighted zero-sum subsequence, then \(S\) has a \(B\)-weighted zero-sum subsequence.

public theorem HasWeightedZeroSumSubseq.mono {n k : ℕ} {A B : Set (ZMod n)}
    {S : Fin k → ZMod n} (hAB : A ⊆ B) (h : HasWeightedZeroSumSubseq A S) :
    HasWeightedZeroSumSubseq B S
Sources
  • Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Introduction.
Uses 1
Statement usesWeighted zero-sum subsequences
20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.