A block of consecutive coordinates orthogonal to \(a\) vectors of \(\mathbb{Z}_2^m\) to Consecutive weighted zero-sum constant for odd weights

TheoremA block of consecutive coordinates orthogonal to \(a\) vectors of \(\mathbb{Z}_2^m\)#●ready to prove

Let \(\mathbb{Z}_2 = \mathbb{Z}/2\mathbb{Z}\), let \(2^a \le m\) and let \(v_1, \dots, v_a \in \mathbb{Z}_2^m\), with coordinates indexed by \(\{0, \dots, m - 1\}\). Then there are indices \(s \le t\) in \(\{0, \dots, m - 1\}\) such that \(\sum_{j = s}^{t} (v_i)_j = 0\) in \(\mathbb{Z}_2\) for every \(i\); that is, the nonzero vector whose ones occupy exactly the positions \(s, \dots, t\) is orthogonal to every \(v_i\).

public theorem_wanted exists_consecutive_orthogonal {a m : ℕ} (hm : 2 ^ a ≤ m)
    (v : Fin a → Fin m → ZMod 2) :
    ∃ s t : Fin m, s ≤ t ∧ ∀ i, ∑ j ∈ Finset.Icc s t, v i j = 0

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Lemma 3.2.

TheoremA block of consecutive integers meeting \(a\) given sets evenly#●ready to prove

Let \(2^a \le m\) and let \(X_1, \dots, X_a\) be finite sets of natural numbers. Then there are integers \(s, t\) with \(1 \le s \le t \le m\) such that \(|\{s, s + 1, \dots, t\} \cap X_i|\) is even for every \(i\).

public theorem_wanted exists_consecutive_even_inter {a m : ℕ} (hm : 2 ^ a ≤ m)
    (X : Fin a → Finset ℕ) :
    ∃ s t : ℕ, 1 ≤ s ∧ s ≤ t ∧ t ≤ m ∧ ∀ i, Even (Finset.Icc s t ∩ X i).card

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Lemma 3.3.

TheoremGriffiths' criterion for unit-weighted zero sums modulo a prime power#●ready to prove

Let \(p\) be a prime, let \(r\) and \(k\) be natural numbers, put \(n = p^r\), and let \(x_1, \dots, x_k \in \mathbb{Z}/n\mathbb{Z}\). Suppose that for each \(i \in [1, r]\) the set \(X_i = \{j : x_j \not\equiv 0 \pmod{p^i}\}\) has an even number of elements. Then there are units \(a_1, \dots, a_k\) of \(\mathbb{Z}/n\mathbb{Z}\) with \(a_1 x_1 + \dots + a_k x_k = 0\).

public theorem_wanted unitWeightedZeroSum_of_even_nonDivisible {p r k : ℕ} (hp : p.Prime)
    (x : Fin k → ZMod (p ^ r))
    (h : ∀ i ∈ Finset.Icc 1 r, Even (Finset.univ.filter fun j => ¬ p ^ i ∣ (x j).val).card) :
    IsUnitWeightedZeroSum (p ^ r) x

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Lemma 3.5.

TheoremDavenport constant of \(\mathbb{Z}_2^a\)#●ready to prove

Let \(\mathbb{Z}_2 = \mathbb{Z}/2\mathbb{Z}\). For every natural number \(a\), the least positive integer \(k\) such that every sequence of \(k\) elements of the group \(\mathbb{Z}_2^a\) has a nonempty subsequence with sum zero is \(a + 1\); that is, the Davenport constant of \(\mathbb{Z}_2^a\) is \(a + 1\).

The paper states this for positive \(a\); for \(a = 0\) both sides equal \(1\).

public theorem_wanted davenport_zmod_two_pow (a : ℕ) :
    IsLeast (davenportSet (ZMod 2) (Fin a → ZMod 2) ({1} : Set (ZMod 2))) (a + 1)

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Theorem 4.1.

TheoremA nonzero vector of \(\mathbb{Z}_2^m\) orthogonal to \(a\) vectors when \(a < m\)#●ready to prove

Let \(\mathbb{Z}_2 = \mathbb{Z}/2\mathbb{Z}\), let \(a + 1 \le m\) and let \(v_1, \dots, v_a \in \mathbb{Z}_2^m\). Then there is a nonzero \(w \in \mathbb{Z}_2^m\) with \(w \cdot v_i = \sum_j w_j (v_i)_j = 0\) in \(\mathbb{Z}_2\) for every \(i\).

public theorem_wanted exists_ne_zero_orthogonal {a m : ℕ} (hm : a + 1 ≤ m)
    (v : Fin a → Fin m → ZMod 2) :
    ∃ w : Fin m → ZMod 2, w ≠ 0 ∧ ∀ i, ∑ j, w j * v i j = 0

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Lemma 4.2.

TheoremA nonempty subset of \(\{1, \dots, m\}\) meeting \(a\) given sets evenly#●ready to prove

Let \(a + 1 \le m\) and let \(X_1, \dots, X_a\) be finite sets of natural numbers. Then there is a nonempty set \(Y \subseteq \{1, \dots, m\}\) such that \(|Y \cap X_i|\) is even for every \(i\).

public theorem_wanted exists_nonempty_even_inter {a m : ℕ} (hm : a + 1 ≤ m)
    (X : Fin a → Finset ℕ) :
    ∃ Y : Finset ℕ, Y.Nonempty ∧ Y ⊆ Finset.Icc 1 m ∧ ∀ i, Even (Y ∩ X i).card

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Lemma 4.3.

TheoremZero-sum subsequences of length \(m\) in \(\mathbb{Z}_2^a\)#●ready to prove

Let \(a\) and \(m\) be natural numbers with \(m\) even and \(2^a \le m\), and write \(\mathbb{Z}_2 = \mathbb{Z}/2\mathbb{Z}\). Every sequence \((x_1, \dots, x_{m+a})\) of length \(m + a\) in \(\mathbb{Z}_2^a\) has a zero-sum subsequence of length \(m\): there is a set \(I\) of exactly \(m\) indices with \(\sum_{i \in I} x_i = 0\).

public theorem_wanted exists_zeroSum_card_zmod_two_pow {a m : ℕ} (hme : Even m) (hm : 2 ^ a ≤ m)
    (x : Fin (m + a) → Fin a → ZMod 2) :
    ∃ I : Finset (Fin (m + a)), I.card = m ∧ ∑ i ∈ I, x i = 0

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Theorem 5.2.

TheoremA weight-\(m\) vector orthogonal to given vectors of \(\mathbb{Z}_2^{m+a}\)#●ready to prove

Let \(a\) and \(m\) be natural numbers with \(m\) even and \(2^a \le m\), write \(\mathbb{Z}_2 = \mathbb{Z}/2\mathbb{Z}\), and let \(v_1, \dots, v_a\) be vectors in \(\mathbb{Z}_2^{m+a}\). Then there is a vector \(w \in \mathbb{Z}_2^{m+a}\) with exactly \(m\) coordinates equal to \(1\) such that \(w \cdot v_i = \sum_j w_j (v_i)_j = 0\) for every \(i\).

public theorem_wanted exists_weight_orthogonal {a m : ℕ} (hme : Even m) (hm : 2 ^ a ≤ m)
    (v : Fin a → Fin (m + a) → ZMod 2) :
    ∃ w : Fin (m + a) → ZMod 2, (Finset.univ.filter fun j => w j = 1).card = m ∧
      ∀ i, ∑ j, w j * v i j = 0

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Lemma 5.3.

TheoremAn \(m\)-subset of \(\{1, \dots, m + a\}\) meeting \(a\) given sets evenly#●ready to prove

Let \(m\) be even with \(2^a \le m\), and let \(X_1, \dots, X_a\) be finite sets of natural numbers. Then there is a set \(Y \subseteq \{1, \dots, m + a\}\) with \(|Y| = m\) such that \(|Y \cap X_i|\) is even for every \(i\).

public theorem_wanted exists_card_even_inter {a m : ℕ} (hme : Even m) (hm : 2 ^ a ≤ m)
    (X : Fin a → Finset ℕ) :
    ∃ Y : Finset ℕ, Y ⊆ Finset.Icc 1 (m + a) ∧ Y.card = m ∧ ∀ i, Even (Y ∩ X i).card

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Lemma 5.4.

TheoremUnit-weighted zero sums of even length in \(\mathbb{Z}_n\)#●ready to prove

Let \(n \ge 1\), let \(\Omega(n)\) be the number of prime factors of \(n\) counted with multiplicity, and let \(m\) be even with \(2^{\Omega(n)} \le m\). Then every sequence \(x_1, \dots, x_{m + \Omega(n)}\) in \(\mathbb{Z}_n = \mathbb{Z}/n\mathbb{Z}\) has a unit-weighted zero-sum subsequence of length \(m\): there are a set \(I \subseteq \{1, \dots, m + \Omega(n)\}\) with \(|I| = m\) and units \(a_i\) of \(\mathbb{Z}_n\) for \(i \in I\) such that \(\sum_{i \in I} a_i x_i = 0\).

public theorem_wanted exists_unitWeightedZeroSum_card {n m : ℕ} (hn : 0 < n) (hme : Even m)
    (hm : 2 ^ Ω n ≤ m) (x : Fin (m + Ω n) → ZMod n) :
    HasUnitWeightedZeroSumOfCard n m x

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Theorem 5.5.

TheoremEvery \(m\)-dimensional subspace of \(\mathbb{Z}_2^{m+a}\) has a vector of weight \(m\)#●ready to prove

Let \(\mathbb{Z}_2 = \mathbb{Z}/2\mathbb{Z}\) and let \(m\) be even with \(2^a \le m\). Then every subspace \(W\) of \(\mathbb{Z}_2^{m+a}\) of dimension \(m\) contains a vector with exactly \(m\) coordinates equal to \(1\).

public theorem_wanted exists_weight_mem_subspace {a m : ℕ} (hme : Even m) (hm : 2 ^ a ≤ m)
    (W : Submodule (ZMod 2) (Fin (m + a) → ZMod 2)) (hW : Module.finrank (ZMod 2) W = m) :
    ∃ v ∈ W, (Finset.univ.filter fun j => v j = 1).card = m

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Corollary 5.7.

TheoremLargest subspaces of \(\mathbb{Z}_2^{m+a}\) with no vector of weight \(m\)#●ready to prove

Let \(a\) and \(m\) be natural numbers with \(m\) even and \(2^a \le m\), and write \(\mathbb{Z}_2 = \mathbb{Z}/2\mathbb{Z}\). The largest dimension of a subspace of \(\mathbb{Z}_2^{m+a}\) containing no vector with exactly \(m\) coordinates equal to \(1\) is \(m - 1\).

public theorem_wanted max_finrank_avoiding_weight {a m : ℕ} (hme : Even m) (hm : 2 ^ a ≤ m) :
    IsGreatest {d : ℕ | ∃ W : Submodule (ZMod 2) (Fin (m + a) → ZMod 2),
      Module.finrank (ZMod 2) W = d ∧
        ∀ v ∈ W, (Finset.univ.filter fun j => v j = 1).card ≠ m} (m - 1)

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Corollary 5.9.

TheoremUnit-weighted Erdős–Ginzburg–Ziv constant of \(\mathbb{Z}_n\) for even \(n\)#●ready to prove

Let \(n\) be a positive even integer, let \(U(n)\) be the set of units of \(\mathbb{Z}_n = \mathbb{Z}/n\mathbb{Z}\), and let \(\Omega(n)\) be the number of prime factors of \(n\) counted with multiplicity. Then \(E_{U(n)}(n) = n + \Omega(n)\), where \(E_{U(n)}(n)\) is the least positive integer \(k\) such that for every sequence \((x_1, \dots, x_k)\) in \(\mathbb{Z}_n\) there are a set \(I\) of exactly \(n\) indices and units \(a_i \in U(n)\) for \(i \in I\) with \(\sum_{i \in I} a_i x_i = 0\).

public theorem_wanted gao_unit_constant_of_even {n : ℕ} (hn : 0 < n) (he : Even n) :
    IsLeast {k : ℕ | 0 < k ∧ ∀ x : Fin k → ZMod n, HasUnitWeightedZeroSumOfCard n n x}
      (n + Ω n)

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Theorem 6.3.

TheoremSequences equivalent to the extremal profile have no unit-weighted zero sum of length \(2^r\)#●ready to prove

Sequences equivalent to the extremal profile have no unit-weighted zero sum of length \(2^r\). Let \(r \ge 1\), \(n = 2^r\) and \(L = n + r - 1\), and let \(U(n)\) be the unit group of \(\mathbb{Z}_n = \mathbb{Z}/n\mathbb{Z}\). Let \(y_1, \dots, y_L \in \mathbb{Z}_n\) be a sequence in which, for each \(i \in \{0, \dots, r - 2\}\), exactly one term equals \(2^i\), an odd number of terms equal \(2^{r-1}\), and every term is \(0\) or \(2^i\) for some \(i < r\). Let \(x_1, \dots, x_L \in \mathbb{Z}_n\) be \(U(n)\)-equivalent to \(y\): there are \(c \in U(n)\), \(b_1, \dots, b_L \in U(n)\) and a permutation \(\sigma\) of \(\{1, \dots, L\}\) with \(c \, y_{\sigma(i)} = b_i x_i\) for all \(i\). Then \(x\) has no \(U(n)\)-weighted zero-sum subsequence of length \(n\): there is no set \(I \subseteq \{1, \dots, L\}\) with \(|I| = n\) together with \(a_i \in U(n)\) for \(i \in I\) such that \(\sum_{i \in I} a_i x_i = 0\).

public theorem_wanted eExtremal_of_unitEquiv_profile {r : ℕ} (hr : 1 ≤ r)
    (x y : Fin (2 ^ r + r - 1) → ZMod (2 ^ r))
    (hy : (∀ i < r - 1, (Finset.univ.filter fun j => y j = 2 ^ i).card = 1) ∧
      Odd (Finset.univ.filter fun j => y j = 2 ^ (r - 1)).card ∧
      ∀ j, y j = 0 ∨ ∃ i < r, y j = 2 ^ i)
    (hxy : ∃ c : ZMod (2 ^ r), IsUnit c ∧ ∃ σ : Equiv.Perm (Fin (2 ^ r + r - 1)),
      ∃ b : Fin (2 ^ r + r - 1) → ZMod (2 ^ r), (∀ i, IsUnit (b i)) ∧
        ∀ i, c * y (σ i) = b i * x i) :
    ¬ HasUnitWeightedZeroSumOfCard (2 ^ r) (2 ^ r) x

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Theorem 6.4.

TheoremStructure of extremal sequences for unit-weighted zero sums of length \(2^r\)#●ready to prove

Let \(r \ge 1\), let \(n = 2^r\), let \(U(n)\) be the set of units of \(\mathbb{Z}_n = \mathbb{Z}/n\mathbb{Z}\), and let \(x = (x_1, \dots, x_{n+r-1})\) be a sequence in \(\mathbb{Z}_n\) with no \(U(n)\)-weighted zero-sum subsequence of length \(n\): there is no set \(I\) of exactly \(n\) indices with units \(a_i \in U(n)\) for \(i \in I\) such that \(\sum_{i \in I} a_i x_i = 0\). Then \(x\) is \(U(n)\)-equivalent to a sequence \((y_1, \dots, y_{n+r-1})\) in \(\mathbb{Z}_n\) in which \(2^i\) occurs exactly once for each \(i \in [0, r - 2]\), \(2^{r-1}\) occurs an odd number of times and every other term is \(0\): there are a unit \(c\), units \(b_1, \dots, b_{n+r-1}\) and a permutation \(\sigma\) of the indices with \(c \, y_{\sigma(i)} = b_i x_i\) for every \(i\).

public theorem_wanted unitEquiv_profile_of_eExtremal {r : ℕ} (hr : 1 ≤ r)
    (x : Fin (2 ^ r + r - 1) → ZMod (2 ^ r))
    (hx : ¬ HasUnitWeightedZeroSumOfCard (2 ^ r) (2 ^ r) x) :
    ∃ y : Fin (2 ^ r + r - 1) → ZMod (2 ^ r),
      ((∀ i < r - 1, (Finset.univ.filter fun j => y j = 2 ^ i).card = 1) ∧
        Odd (Finset.univ.filter fun j => y j = 2 ^ (r - 1)).card ∧
        ∀ j, y j = 0 ∨ ∃ i < r, y j = 2 ^ i) ∧
      ∃ c : ZMod (2 ^ r), IsUnit c ∧ ∃ σ : Equiv.Perm (Fin (2 ^ r + r - 1)),
        ∃ b : Fin (2 ^ r + r - 1) → ZMod (2 ^ r), (∀ i, IsUnit (b i)) ∧
          ∀ i, c * y (σ i) = b i * x i

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Theorem 6.6.

TheoremLuca's lemma on unit-weighted zero sums modulo \(2^r\)#●ready to prove

Let \(r\) and \(k\) be natural numbers and let \(x_1, \dots, x_k \in \mathbb{Z}/2^r\mathbb{Z}\). If the number of indices \(j\) for which \(x_j\) is a unit is even and nonzero, then there are units \(a_1, \dots, a_k\) of \(\mathbb{Z}/2^r\mathbb{Z}\) with \(a_1 x_1 + \dots + a_k x_k = 0\).

public theorem_wanted unitWeightedZeroSum_of_even_units {r k : ℕ} (x : Fin k → ZMod (2 ^ r))
    (h0 : (Finset.univ.filter fun j => IsUnit (x j)).card ≠ 0)
    (he : Even (Finset.univ.filter fun j => IsUnit (x j)).card) :
    IsUnitWeightedZeroSum (2 ^ r) x

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Lemma 6.5.

TheoremUnit-weighted zero sums of multiples of a prime#●ready to prove

Let \(p\) be a prime, let \(n'\) and \(k\) be natural numbers, put \(n = p n'\), and let \(z_1, \dots, z_k \in \mathbb{Z}/n\mathbb{Z}\). Write \(\bar z_i\) for the reduction of \(z_i\) modulo \(n'\). If there are units \(a_1, \dots, a_k\) of \(\mathbb{Z}/n'\mathbb{Z}\) with \(\sum_i a_i \bar z_i = 0\), then there are units \(b_1, \dots, b_k\) of \(\mathbb{Z}/n\mathbb{Z}\) with \(\sum_i b_i \, p z_i = 0\).

In the source the sequence \((p z_1, \dots, p z_k)\) determines the \(z_i\) only modulo \(n'\), so the hypothesis does not depend on the choice of the \(z_i\).

public theorem_wanted unitWeightedZeroSum_of_div_prime {p n' k : ℕ} (hp : p.Prime)
    (z : Fin k → ZMod (p * n'))
    (h : IsUnitWeightedZeroSum n' (fun i => ZMod.castHom (dvd_mul_left n' p) (ZMod n') (z i))) :
    IsUnitWeightedZeroSum (p * n') (fun i => (p : ZMod (p * n')) * z i)

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Lemma 6.7.

TheoremHalving consecutive unit-weighted zero-sum free sequences modulo a power of two#●ready to prove

Let \(s \ge 0\), \(n = 2^{s+1}\) and \(n' = 2^s\). Say that a sequence \(y_1, \dots, y_L\) in \(\mathbb{Z}_m\) has no consecutive unit-weighted zero-sum if there are no indices \(1 \le i \le j \le L\) and units \(a_i, \dots, a_j\) of \(\mathbb{Z}_m\) with \(a_i y_i + \dots + a_j y_j = 0\). For a sequence \(x_1, \dots, x_{n-1}\) in \(\mathbb{Z}_n\), let \(r_l \in \{0, \dots, n - 1\}\) be the representative of \(x_l\) and let \(\bar x_l \in \mathbb{Z}_{n'}\) be the residue of \(\lfloor r_l / 2 \rfloor\). Then \(x_1, \dots, x_{n-1}\) has no consecutive unit-weighted zero-sum if and only if \(r_l\) is even for every \(l \ne n'\), \(r_{n'}\) is odd, and neither of the sequences \(\bar x_1, \dots, \bar x_{n'-1}\) and \(\bar x_{n'+1}, \dots, \bar x_{n-1}\) in \(\mathbb{Z}_{n'}\) has a consecutive unit-weighted zero-sum.

Write \(U(n)\) for the unit group of \(\mathbb{Z}_n\) and \(C_{U(n)}(n)\) for the least positive \(k\) such that every sequence of length \(k\) in \(\mathbb{Z}_n\) has a consecutive unit-weighted zero-sum. Since \(C_{U(n)}(n) = n\), the sequences on the left are the \(C\)-extremal sequences for \(U(n)\): those of length \(C_{U(n)}(n) - 1\) with no consecutive unit-weighted zero-sum.

public theorem_wanted cExtremal_iff_halves (s : ℕ) (x : ℕ → ZMod (2 ^ (s + 1))) :
    (NoConsecutiveUnitWeightedZeroSum (2 ^ (s + 1)) (2 ^ (s + 1) - 1) x) ↔
      (∀ j < 2 ^ (s + 1) - 1, j ≠ 2 ^ s - 1 → Even (x j).val) ∧ Odd (x (2 ^ s - 1)).val ∧
        (NoConsecutiveUnitWeightedZeroSum (2 ^ s) (2 ^ s - 1)
          (fun j => (((x j).val / 2 : ℕ) : ZMod (2 ^ s)))) ∧
        (NoConsecutiveUnitWeightedZeroSum (2 ^ s) (2 ^ s - 1)
          (fun j => (((x (2 ^ s + j)).val / 2 : ℕ) : ZMod (2 ^ s))))

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Theorem 6.8.

TheoremConsecutive weighted zero-sum constant for interval weights#●ready to prove

Let \(n \ge 2\) and \(1 \le r \le n - 1\), and let \(A \subseteq \mathbb{Z}_n\) be the set of residues of \(1, 2, \dots, r\). Let \(C_A(n)\) be the least positive integer \(k\) such that every sequence \(x_1, \dots, x_k\) in \(\mathbb{Z}_n\) has indices \(s \le t\) and weights \(a_s, \dots, a_t \in A\) with \(a_s x_s + \dots + a_t x_t = 0\). Then \(C_A(n) = \lceil n / r \rceil\).

public theorem_wanted consecutive_interval_weights {n r : ℕ} (hn : 2 ≤ n) (hr : 1 ≤ r)
    (hrn : r ≤ n - 1) :
    IsLeast (consecutiveSet (ZMod n) (ZMod n) ((fun j : ℕ => (j : ZMod n)) '' Set.Icc 1 r))
      ⌈(n : ℚ) / r⌉₊

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Theorem 7.1.

TheoremConsecutive weighted zero-sum constant for odd weights#●ready to prove

Let \(n\) be a positive even integer, let \(2^r\) be the largest power of \(2\) dividing \(n\) and let \(m = n / 2^r\). Let \(A \subseteq \mathbb{Z}_n\) contain the residue of \(m\) and consist of odd elements (residues whose representative in \(\{0, \dots, n - 1\}\) is odd). Let \(C_A(n)\) be the least positive integer \(k\) such that every sequence \(x_1, \dots, x_k\) in \(\mathbb{Z}_n\) has indices \(s \le t\) and weights \(a_s, \dots, a_t \in A\) with \(a_s x_s + \dots + a_t x_t = 0\). Then \(C_A(n) = 2^r\).

public theorem_wanted consecutive_odd_weights {n : ℕ} (hn : 0 < n) (he : Even n)
    (A : Set (ZMod n)) (hmA : ((n / 2 ^ padicValNat 2 n : ℕ) : ZMod n) ∈ A)
    (hAB : A ⊆ {x : ZMod n | Odd x.val}) :
    IsLeast (consecutiveSet (ZMod n) (ZMod n) A) (2 ^ padicValNat 2 n)

Sources

• Santanu Mondal, Krishnendu Paul and Shameek Paul, On Unit-Weighted Zero-Sum Constants of ℤ_n, INTEGERS 24 (2024), Article A38, Theorem 7.2.

20 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.