Weight sets with weighted Davenport constant \(m\) on \(\mathbb{Z}/n\mathbb{Z}\) to Three-term sums of square-weighted units cover \(\mathbb{Z}_{p^r}\)

TheoremWeight sets with weighted Davenport constant \(m\) on \(\mathbb{Z}/n\mathbb{Z}\)#●ready to prove

Let \(n \ge 2\) be a natural number and \(m \ge 2\) a divisor of \(n\). Every finite set \(A\) of natural numbers with \(n/m \in A \subseteq \{1, \dots, \lceil n/(m-1) \rceil - 1\}\) has \(A\)-weighted Davenport constant \(D_A(\mathbb{Z}/n\mathbb{Z}) = m\).

public theorem_wanted weightedDavenport_zmod_of_dvd (m n : ℕ) (hm : 2 ≤ m) (hn : 2 ≤ n)
    (hdvd : m ∣ n) (A : Finset ℕ) (hmem : n / m ∈ A)
    (hsub : A ⊆ Finset.Icc 1 (n ⌈/⌉ (m - 1) - 1)) :
    weightedDavenport A (ZMod n) = ((m : ℕ) : ℕ∞)
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Theorem 5.
Uses 1
Statement usesWeighted Davenport constant

TheoremWeighted Davenport constant of \(\mathbb{Z}/n\mathbb{Z}\) for the weights \(\{1, \dots, r\}\)#●ready to prove

Let \(n\) and \(r\) be natural numbers with \(1 < r < n\) and let \(A = \{1, \dots, r\}\). Then the \(A\)-weighted Davenport constant of \(\mathbb{Z}/n\mathbb{Z}\) is \(D_A(\mathbb{Z}/n\mathbb{Z}) = \lceil n/r \rceil\).

public theorem_wanted weightedDavenport_zmod_Icc (n r : ℕ) (hr : 1 < r) (hrn : r < n) :
    weightedDavenport (Finset.Icc 1 r) (ZMod n) = ((n ⌈/⌉ r : ℕ) : ℕ∞)
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Corollary 1, first part.
Uses 1
Statement usesWeighted Davenport constant

TheoremInitial-interval weights with weighted Davenport constant \(m\)#●ready to prove

Let \(m, n \ge 2\) be natural numbers with \(m \mid n\) and put \(r = \lceil n/(m-1) \rceil - 1\). Then the \(\{1, \dots, r\}\)-weighted Davenport constant of \(\mathbb{Z}/n\mathbb{Z}\) is \(D_{\{1, \dots, r\}}(\mathbb{Z}/n\mathbb{Z}) = m\).

public theorem_wanted weightedDavenport_zmod_Icc_of_dvd (m n : ℕ) (hm : 2 ≤ m) (hn : 2 ≤ n)
    (hdvd : m ∣ n) :
    weightedDavenport (Finset.Icc 1 (n ⌈/⌉ (m - 1) - 1)) (ZMod n) = ((m : ℕ) : ℕ∞)
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Corollary 1, second part.
Uses 1
Statement usesWeighted Davenport constant

TheoremLong weighted zero-sum free sequences in groups of rank two#●ready to prove

Let \(m, n \ge 2\) be natural numbers with \(m \mid n\), let \(k \ge 1\) and put \(\alpha = \lceil n/(m-1) \rceil - 1\). Then there is a sequence \(s\) over \(\mathbb{Z}/n\mathbb{Z} \oplus \mathbb{Z}/kn\mathbb{Z}\) of length \(m + \lceil kn/\alpha \rceil - 2\) that is \(\{1, \dots, \alpha\}\)-weighted zero-sum free: for every non-empty set \(I\) of positions and all weights \(a_i \in \{1, \dots, \alpha\}\), the weighted sum \(\sum_{i \in I} a_i s_i\) is non-zero.

In particular the \(\{1, \dots, \alpha\}\)-weighted Davenport constant of \(\mathbb{Z}/n\mathbb{Z} \oplus \mathbb{Z}/kn\mathbb{Z}\) is at least \(m + \lceil kn/\alpha \rceil - 1\).

public theorem_wanted exists_weightedZeroSumFree_zmod_prod (m n k : ℕ) (hm : 2 ≤ m)
    (hn : 2 ≤ n) (hdvd : m ∣ n) (hk : 1 ≤ k) :
    ∃ s : List (ZMod n × ZMod (k * n)),
      s.length = m + (k * n) ⌈/⌉ (n ⌈/⌉ (m - 1) - 1) - 2 ∧
        IsWeightedZeroSumFree (Finset.Icc 1 (n ⌈/⌉ (m - 1) - 1)) s
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Lemma 2.
Uses 1
Statement usesWeighted zero-sum free sequences

TheoremWeight sets with prescribed weighted Davenport constant on \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/kn\mathbb{Z}\), divisible case#●ready to prove

Weight sets with prescribed weighted Davenport constant on \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/kn\mathbb{Z}\), divisible case. Let \(n \ge 2\) and \(k \ge 1\) be natural numbers, let \(m \ge 2\) be a divisor of \(n\), let \(\alpha = \lceil n/(m-1) \rceil - 1\), and suppose that \(\alpha\) divides \(n\). Then for every finite set \(A\) of natural numbers with \(n/m \in A \subseteq \{1, \dots, \alpha\}\), the \(A\)-weighted Davenport constant of \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/kn\mathbb{Z}\) is \(D_A(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/kn\mathbb{Z}) = m + \lceil kn/\alpha \rceil - 1\).

public theorem_wanted weightedDavenport_zmod_prod_of_dvd (m n k : ℕ) (hm : 2 ≤ m)
    (hn : 2 ≤ n) (hdvd : m ∣ n) (A : Finset ℕ) (hmem : n / m ∈ A)
    (hsub : A ⊆ Finset.Icc 1 (n ⌈/⌉ (m - 1) - 1)) (hα : n ⌈/⌉ (m - 1) - 1 ∣ n)
    (hk : 1 ≤ k) :
    weightedDavenport A (ZMod n × ZMod (k * n)) =
      ((m + (k * n) ⌈/⌉ (n ⌈/⌉ (m - 1) - 1) - 1 : ℕ) : ℕ∞)
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Theorem 6(i).
Uses 1
Statement usesWeighted Davenport constant

TheoremWeight sets with prescribed weighted Davenport constant on \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/kn\mathbb{Z}\), non-divisible case#●ready to prove

Weight sets with prescribed weighted Davenport constant on \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/kn\mathbb{Z}\), non-divisible case. Let \(n \ge 2\) and \(k \ge 1\) be natural numbers, let \(m \ge 2\) be a divisor of \(n\), let \(\alpha = \lceil n/(m-1) \rceil - 1\), and suppose that \(\alpha\) does not divide \(n\). Let \(r\) be the remainder of \(n\) modulo \(\alpha\), so that \(1 \le r < \alpha\), and suppose that \((k - 1)\alpha < kr\). Then for every finite set \(A\) of natural numbers with \(n/m \in A \subseteq \{1, \dots, \alpha\}\), the \(A\)-weighted Davenport constant of \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/kn\mathbb{Z}\) is \(D_A(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/kn\mathbb{Z}) = m + \lceil kn/\alpha \rceil - 1\).

public theorem_wanted weightedDavenport_zmod_prod_of_not_dvd (m n k : ℕ) (hm : 2 ≤ m)
    (hn : 2 ≤ n) (hdvd : m ∣ n) (A : Finset ℕ) (hmem : n / m ∈ A)
    (hsub : A ⊆ Finset.Icc 1 (n ⌈/⌉ (m - 1) - 1)) (hr : 0 < n % (n ⌈/⌉ (m - 1) - 1))
    (hk : 1 ≤ k)
    (hkr : (k - 1) * (n ⌈/⌉ (m - 1) - 1) < k * (n % (n ⌈/⌉ (m - 1) - 1))) :
    weightedDavenport A (ZMod n × ZMod (k * n)) =
      ((m + (k * n) ⌈/⌉ (n ⌈/⌉ (m - 1) - 1) - 1 : ℕ) : ℕ∞)
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Theorem 6(ii).
Uses 1
Statement usesWeighted Davenport constant

TheoremWeight sets with weighted Davenport constant \(2m - 1\) on \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z}\)#●ready to prove

Weight sets with weighted Davenport constant \(2m - 1\) on \(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z}\). Let \(n \ge 2\) be a natural number and \(m \ge 2\) a divisor of \(n\). Every finite set \(A\) of natural numbers with \(n/m \in A \subseteq \{1, \dots, \lceil n/(m-1) \rceil - 1\}\) has \(A\)-weighted Davenport constant \(D_A(\mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z}) = 2m - 1\).

public theorem_wanted weightedDavenport_zmod_prod_self_of_dvd (m n : ℕ) (hm : 2 ≤ m)
    (hn : 2 ≤ n) (hdvd : m ∣ n) (A : Finset ℕ) (hmem : n / m ∈ A)
    (hsub : A ⊆ Finset.Icc 1 (n ⌈/⌉ (m - 1) - 1)) :
    weightedDavenport A (ZMod n × ZMod n) = ((2 * m - 1 : ℕ) : ℕ∞)
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Corollary 2.
Uses 1
Statement usesWeighted Davenport constant

TheoremLong weighted zero-sum free sequences in abelian \(p\)-groups#●ready to prove

Let \(p\) be a prime, let \(r \ge 1\), let \(e_1 \le e_2 \le \dots \le e_r\) be natural numbers and let \(G = \mathbb{Z}/p^{e_1}\mathbb{Z} \oplus \dots \oplus \mathbb{Z}/p^{e_r}\mathbb{Z}\). Let \(c\) be a natural number with \(1 \le c \le e_1\) and put \(\beta = \lceil p^{e_1}/(p^c - 1) \rceil - 1\). Then there is a sequence \(s\) over \(G\) of length \(\sum_{i=1}^{r} (\lceil p^{e_i}/\beta \rceil - 1)\) that is \(\{1, \dots, \beta\}\)-weighted zero-sum free: for every non-empty set \(I\) of positions and all weights \(a_i \in \{1, \dots, \beta\}\), the weighted sum \(\sum_{i \in I} a_i s_i\) is non-zero.

In particular the \(\{1, \dots, \beta\}\)-weighted Davenport constant of \(G\) is at least \(1 + \sum_{i=1}^{r} (\lceil p^{e_i}/\beta \rceil - 1)\).

public theorem_wanted exists_weightedZeroSumFree_pi_zmod_prime_pow (p r c : ℕ)
    (hp : p.Prime) (hr : 0 < r) (e : Fin r → ℕ) (hmono : Monotone e) (hc : 1 ≤ c)
    (hce : c ≤ e ⟨0, hr⟩) :
    ∃ s : List ((i : Fin r) → ZMod (p ^ e i)),
      s.length = ∑ i, (p ^ e i ⌈/⌉ (p ^ e ⟨0, hr⟩ ⌈/⌉ (p ^ c - 1) - 1) - 1) ∧
        IsWeightedZeroSumFree (Finset.Icc 1 (p ^ e ⟨0, hr⟩ ⌈/⌉ (p ^ c - 1) - 1)) s
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Lemma 3.
Uses 1
Statement usesWeighted zero-sum free sequences

TheoremWeighted Davenport constant of abelian \(p\)-groups, divisible case#●ready to prove

Let \(p\) be a prime, let \(r \ge 1\), let \(e_1 \le e_2 \le \dots \le e_r\) be natural numbers and let \(G = \mathbb{Z}/p^{e_1}\mathbb{Z} \oplus \dots \oplus \mathbb{Z}/p^{e_r}\mathbb{Z}\). Let \(c\) be a natural number with \(1 \le c \le e_1\), put \(\beta = \lceil p^{e_1}/(p^c - 1) \rceil - 1\) and let \(A\) be a finite set of natural numbers with \(p^{e_1 - c} \in A \subseteq \{1, \dots, \beta\}\). If \(\beta \mid p^{e_1}\), then the \(A\)-weighted Davenport constant of \(G\) is \(D_A(G) = 1 + \sum_{i=1}^{r} (\lceil p^{e_i}/\beta \rceil - 1)\).

public theorem_wanted weightedDavenport_pi_zmod_prime_pow_of_dvd (p r c : ℕ) (hp : p.Prime)
    (hr : 0 < r) (e : Fin r → ℕ) (hmono : Monotone e) (hc : 1 ≤ c) (hce : c ≤ e ⟨0, hr⟩)
    (A : Finset ℕ) (hmem : p ^ (e ⟨0, hr⟩ - c) ∈ A)
    (hsub : A ⊆ Finset.Icc 1 (p ^ e ⟨0, hr⟩ ⌈/⌉ (p ^ c - 1) - 1))
    (hβ : p ^ e ⟨0, hr⟩ ⌈/⌉ (p ^ c - 1) - 1 ∣ p ^ e ⟨0, hr⟩) :
    weightedDavenport A ((i : Fin r) → ZMod (p ^ e i)) =
      ((1 + ∑ i, (p ^ e i ⌈/⌉ (p ^ e ⟨0, hr⟩ ⌈/⌉ (p ^ c - 1) - 1) - 1) : ℕ) : ℕ∞)
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Theorem 7(i).
Uses 1
Statement usesWeighted Davenport constant

TheoremWeighted Davenport constant of abelian \(p\)-groups, non-divisible case#●ready to prove

Let \(p\) be a prime, let \(r \ge 1\), let \(e_1 \le e_2 \le \dots \le e_r\) be natural numbers and let \(G = \mathbb{Z}/p^{e_1}\mathbb{Z} \oplus \dots \oplus \mathbb{Z}/p^{e_r}\mathbb{Z}\). Let \(c\) be a natural number with \(1 \le c \le e_1\), put \(\beta = \lceil p^{e_1}/(p^c - 1) \rceil - 1\) and let \(A\) be a finite set of natural numbers with \(p^{e_1 - c} \in A \subseteq \{1, \dots, \beta\}\). Suppose that \(\beta \nmid p^{e_1}\) and let \(s\) be the remainder of \(p^{e_1}\) modulo \(\beta\), so that \(1 \le s < \beta\). If \((p^{e_j - e_1} - 1)\beta < s\,p^{e_j - e_1}\) for every \(j \in \{2, \dots, r\}\), then the \(A\)-weighted Davenport constant of \(G\) is \(D_A(G) = 1 + \sum_{i=1}^{r} (\lceil p^{e_i}/\beta \rceil - 1)\).

public theorem_wanted weightedDavenport_pi_zmod_prime_pow_of_not_dvd (p r c : ℕ)
    (hp : p.Prime) (hr : 0 < r) (e : Fin r → ℕ) (hmono : Monotone e) (hc : 1 ≤ c)
    (hce : c ≤ e ⟨0, hr⟩) (A : Finset ℕ) (hmem : p ^ (e ⟨0, hr⟩ - c) ∈ A)
    (hsub : A ⊆ Finset.Icc 1 (p ^ e ⟨0, hr⟩ ⌈/⌉ (p ^ c - 1) - 1))
    (hs : 0 < p ^ e ⟨0, hr⟩ % (p ^ e ⟨0, hr⟩ ⌈/⌉ (p ^ c - 1) - 1))
    (hineq : ∀ j : Fin r, 0 < j.val →
      (p ^ (e j - e ⟨0, hr⟩) - 1) * (p ^ e ⟨0, hr⟩ ⌈/⌉ (p ^ c - 1) - 1) <
        p ^ e ⟨0, hr⟩ % (p ^ e ⟨0, hr⟩ ⌈/⌉ (p ^ c - 1) - 1) * p ^ (e j - e ⟨0, hr⟩)) :
    weightedDavenport A ((i : Fin r) → ZMod (p ^ e i)) =
      ((1 + ∑ i, (p ^ e i ⌈/⌉ (p ^ e ⟨0, hr⟩ ⌈/⌉ (p ^ c - 1) - 1) - 1) : ℕ) : ℕ∞)
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Theorem 7(ii).
Uses 1
Statement usesWeighted Davenport constant

TheoremWeighted Davenport constant of \((\mathbb{Z}/p^e\mathbb{Z})^r\)#●ready to prove

Let \(p\) be a prime and let \(a, e, r\) be natural numbers with \(1 \le a \le e\) and \(r \ge 1\). Let \(A\) be a finite set of natural numbers with \(p^{e-a} \in A \subseteq \{1, \dots, \lceil p^e/(p^a - 1) \rceil - 1\}\). Then the \(A\)-weighted Davenport constant of \((\mathbb{Z}/p^e\mathbb{Z})^r\) is \(D_A((\mathbb{Z}/p^e\mathbb{Z})^r) = 1 + r(p^a - 1)\).

public theorem_wanted weightedDavenport_pi_zmod_prime_pow_const (p e a r : ℕ) (hp : p.Prime)
    (ha : 1 ≤ a) (hae : a ≤ e) (hr : 1 ≤ r) (A : Finset ℕ) (hmem : p ^ (e - a) ∈ A)
    (hsub : A ⊆ Finset.Icc 1 (p ^ e ⌈/⌉ (p ^ a - 1) - 1)) :
    weightedDavenport A ((_ : Fin r) → ZMod (p ^ e)) = ((1 + r * (p ^ a - 1) : ℕ) : ℕ∞)
Sources
  • Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Corollary 3.
Uses 1
Statement usesWeighted Davenport constant

TheoremUnit-weighted zero-sum constants of \(\mathbb{Z}_n\)#●ready to prove

Let \(n\) be a positive 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 \(D_{U(n)}(n) = \Omega(n) + 1\) and \(C_{U(n)}(n) = 2^{\Omega(n)}\). Here \(D_{U(n)}(n)\) is the least positive integer \(k\) such that every sequence \((x_1, \dots, x_k)\) in \(\mathbb{Z}_n\) has a nonempty set \(I\) of indices and units \(a_i \in U(n)\) for \(i \in I\) with \(\sum_{i \in I} a_i x_i = 0\), and \(C_{U(n)}(n)\) is defined in the same way with \(I\) restricted to a block \(\{s, s+1, \dots, t\}\) of consecutive indices.

public theorem_wanted unit_weighted_zero_sum_constants (n : ℕ) (hn : 0 < n) :
    IsLeast (davenportSet n (unitSet n)) (Ω n + 1) ∧
      IsLeast (consecutiveSet n (unitSet n)) (2 ^ Ω n)
Sources
  • Santanu Mondal, Krishnendu Paul and Shameek Paul, Zero-Sum Constants Related to the Jacobi Symbol, Journal of Integer Sequences 27 (2024), Article 24.1.7, Theorem 4 (jis-2024-24.1.7-thm-4).

TheoremQuadratic-residue-weighted zero-sum constants modulo a prime#●ready to prove

Let \(p\) be an odd prime and let \(Q_p\) be the set of squares of units of \(\mathbb{Z}_p = \mathbb{Z}/p\mathbb{Z}\). Then \(C_{Q_p}(p) = D_{Q_p}(p) = 3\). Here \(D_{Q_p}(p)\) is the least positive integer \(k\) such that every sequence \((x_1, \dots, x_k)\) in \(\mathbb{Z}_p\) has a nonempty set \(I\) of indices and weights \(a_i \in Q_p\) for \(i \in I\) with \(\sum_{i \in I} a_i x_i = 0\), and \(C_{Q_p}(p)\) is defined in the same way with \(I\) restricted to a block \(\{s, s+1, \dots, t\}\) of consecutive indices.

public theorem_wanted quadratic_residue_weighted_zero_sum_constants (p : ℕ) (hp : p.Prime)
    (hp2 : p ≠ 2) :
    IsLeast (consecutiveSet p (unitSqSet p)) 3 ∧ IsLeast (davenportSet p (unitSqSet p)) 3
Sources
  • Santanu Mondal, Krishnendu Paul and Shameek Paul, Zero-Sum Constants Related to the Jacobi Symbol, Journal of Integer Sequences 27 (2024), Article 24.1.7, Theorem 5 (jis-2024-24.1.7-thm-5).

TheoremProduct lower bound for the consecutive weighted zero-sum constant#●ready to prove

For a natural number \(n\) and \(A \subseteq \mathbb{Z}/n\mathbb{Z}\), let \(C_A(n)\) denote the least positive integer \(k\) such that every sequence \((x_1, \dots, x_k)\) in \(\mathbb{Z}/n\mathbb{Z}\) has a block of consecutive terms \(x_s, \dots, x_t\) with \(s \le t\) and weights \(a_s, \dots, a_t \in A\) such that \(a_s x_s + \dots + a_t x_t = 0\). Let \(m\) and \(q\) be natural numbers and let \(A \subseteq \mathbb{Z}/mq\mathbb{Z}\), \(B \subseteq \mathbb{Z}/m\mathbb{Z}\) and \(C \subseteq \mathbb{Z}/q\mathbb{Z}\) be such that the reduction map \(\mathbb{Z}/mq\mathbb{Z} \to \mathbb{Z}/m\mathbb{Z}\) sends \(A\) into \(B\) and the reduction map \(\mathbb{Z}/mq\mathbb{Z} \to \mathbb{Z}/q\mathbb{Z}\) sends \(A\) into \(C\). If \(C_A(mq)\), \(C_B(m)\) and \(C_C(q)\) exist, then \(C_A(mq) \ge C_B(m)\,C_C(q)\).

public theorem_wanted consecutive_constant_mul_le (m q : ℕ) (A : Set (ZMod (m * q)))
    (B : Set (ZMod m)) (C : Set (ZMod q))
    (hB : ZMod.castHom (dvd_mul_right m q) (ZMod m) '' A ⊆ B)
    (hC : ZMod.castHom (dvd_mul_left q m) (ZMod q) '' A ⊆ C) (cA cB cC : ℕ)
    (hA : IsLeast (consecutiveSet (m * q) A) cA) (hBc : IsLeast (consecutiveSet m B) cB)
    (hCc : IsLeast (consecutiveSet q C) cC) :
    cB * cC ≤ cA
Sources
  • Santanu Mondal, Krishnendu Paul and Shameek Paul, Zero-Sum Constants Related to the Jacobi Symbol, Journal of Integer Sequences 27 (2024), Article 24.1.7, Lemma 8 (jis-2024-24.1.7-lem-8).

TheoremLower bound for the weighted Davenport constant of a product modulus#●ready to prove

For a natural number \(n\) and \(A \subseteq \mathbb{Z}/n\mathbb{Z}\), let \(D_A(n)\) denote the least positive integer \(k\) such that every sequence \((x_1, \dots, x_k)\) in \(\mathbb{Z}/n\mathbb{Z}\) has a nonempty set \(J\) of indices and weights \(a_i \in A\) for \(i \in J\) with \(\sum_{i \in J} a_i x_i = 0\). Let \(m\) and \(q\) be natural numbers and let \(A \subseteq \mathbb{Z}/mq\mathbb{Z}\), \(B \subseteq \mathbb{Z}/m\mathbb{Z}\) and \(C \subseteq \mathbb{Z}/q\mathbb{Z}\) be such that the reduction map \(\mathbb{Z}/mq\mathbb{Z} \to \mathbb{Z}/m\mathbb{Z}\) sends \(A\) into \(B\) and the reduction map \(\mathbb{Z}/mq\mathbb{Z} \to \mathbb{Z}/q\mathbb{Z}\) sends \(A\) into \(C\). If \(D_A(mq)\), \(D_B(m)\) and \(D_C(q)\) exist, then \(D_A(mq) \ge D_B(m) + D_C(q) - 1\).

public theorem_wanted davenport_constant_add_le (m q : ℕ) (A : Set (ZMod (m * q)))
    (B : Set (ZMod m)) (C : Set (ZMod q))
    (hB : ZMod.castHom (dvd_mul_right m q) (ZMod m) '' A ⊆ B)
    (hC : ZMod.castHom (dvd_mul_left q m) (ZMod q) '' A ⊆ C) (dA dB dC : ℕ)
    (hA : IsLeast (davenportSet (m * q) A) dA) (hBd : IsLeast (davenportSet m B) dB)
    (hCd : IsLeast (davenportSet q C) dC) :
    dB + dC - 1 ≤ dA
Sources
  • Santanu Mondal, Krishnendu Paul and Shameek Paul, Zero-Sum Constants Related to the Jacobi Symbol, Journal of Integer Sequences 27 (2024), Article 24.1.7, Lemma 9 (jis-2024-24.1.7-lem-9).

TheoremThe index of the Jacobi symbol kernel#●ready to prove

Let \(n\) be an odd natural number, let \(U(n)\) be the group of units of \(\mathbb{Z}_n = \mathbb{Z}/n\mathbb{Z}\), and let \(S(n) = \{u \in U(n) : (u/n) = 1\}\), where \((u/n)\) is the Jacobi symbol \((a/n)\) of the representative \(0 \le a < n\) of \(u\). If \(n\) is not a perfect square, then \(S(n)\) is a subgroup of \(U(n)\) of index \(2\). If \(n\) is a perfect square, then \(S(n) = U(n)\).

public theorem_wanted jacobi_kernel_index_two (n : ℕ) (hn : Odd n) :
    (¬ IsSquare n → ∃ H : Subgroup (ZMod n)ˣ,
      (∀ u : (ZMod n)ˣ, u ∈ H ↔ jacobiSym (((u : ZMod n).val : ℕ) : ℤ) n = 1) ∧
        H.index = 2) ∧
    (IsSquare n → ∀ u : (ZMod n)ˣ, jacobiSym (((u : ZMod n).val : ℕ) : ℤ) n = 1)
Sources
  • Santanu Mondal, Krishnendu Paul and Shameek Paul, Zero-Sum Constants Related to the Jacobi Symbol, Journal of Integer Sequences 27 (2024), Article 24.1.7, Proposition 11 (jis-2024-24.1.7-prop-11).

TheoremUnits lift to the kernel of the Jacobi symbol across a non-square coprime factor#●ready to prove

Let \(d\) and \(n'\) be coprime natural numbers such that \(d n'\) is odd and \(d\) is not a perfect square, and put \(n = d n'\). Then every unit \(y\) of \(\mathbb{Z}/n'\mathbb{Z}\) is the reduction modulo \(n'\) of a unit \(x\) of \(\mathbb{Z}/n\mathbb{Z}\) whose least nonnegative representative \(v\) has Jacobi symbol \(\left(\frac{v}{n}\right) = 1\).

public theorem_wanted units_subset_image_jacobi_kernel (d n' : ℕ) (hn : Odd (d * n'))
    (hd : ¬ IsSquare d) (hcop : Nat.Coprime d n') (y : ZMod n') (hy : IsUnit y) :
    ∃ x ∈ jacobiOneSet (d * n'), ZMod.castHom (dvd_mul_left n' d) (ZMod n') x = y
Sources
  • Santanu Mondal, Krishnendu Paul and Shameek Paul, Zero-Sum Constants Related to the Jacobi Symbol, Journal of Integer Sequences 27 (2024), Article 24.1.7, Lemma 14 (jis-2024-24.1.7-lem-14).

TheoremLifting weighted zero sums along a coprime factor#●ready to prove

Let \(d\) and \(n'\) be coprime natural numbers, put \(n = d n'\), and let \(f : \mathbb{Z}/n\mathbb{Z} \to \mathbb{Z}/n'\mathbb{Z}\) be reduction modulo \(n'\). Let \(A \subseteq \mathbb{Z}/n\mathbb{Z}\) and \(A' \subseteq \mathbb{Z}/n'\mathbb{Z}\) with \(A' \subseteq f(A)\), and let \(x_1, \dots, x_k \in \mathbb{Z}/n\mathbb{Z}\) each be divisible by \(d\) in \(\mathbb{Z}/n\mathbb{Z}\). If there are \(a'_1, \dots, a'_k \in A'\) with \(a'_1 f(x_1) + \dots + a'_k f(x_k) = 0\), then there are \(a_1, \dots, a_k \in A\) with \(a_1 x_1 + \dots + a_k x_k = 0\).

public theorem_wanted weighted_zero_sum_of_image (d n' k : ℕ) (hcop : Nat.Coprime d n')
    (x : Fin k → ZMod (d * n')) (hx : ∀ i, (d : ZMod (d * n')) ∣ x i)
    (A : Set (ZMod (d * n'))) (A' : Set (ZMod n'))
    (hA : A' ⊆ ZMod.castHom (dvd_mul_left n' d) (ZMod n') '' A)
    (h : IsWeightedZeroSum n' k A' (fun i => ZMod.castHom (dvd_mul_left n' d) (ZMod n') (x i))) :
    IsWeightedZeroSum (d * n') k A x
Sources
  • Santanu Mondal, Krishnendu Paul and Shameek Paul, Zero-Sum Constants Related to the Jacobi Symbol, Journal of Integer Sequences 27 (2024), Article 24.1.7, Lemma 15 (jis-2024-24.1.7-lem-15).

TheoremUnit-weighted zero sums modulo an odd prime power#●ready to prove

Let \(p\) be an odd prime, let \(r\) and \(k\) be natural numbers, and let \(x_1, \dots, x_k \in \mathbb{Z}/p^r\mathbb{Z}\). Suppose that for at least two indices \(i\) the least nonnegative representative of \(x_i\) is coprime to \(p\). Then there are units \(a_1, \dots, a_k\) of \(\mathbb{Z}/p^r\mathbb{Z}\) with \(a_1 x_1 + \dots + a_k x_k = 0\).

public theorem_wanted unit_weighted_zero_sum_prime_power (p r k : ℕ) (hp : p.Prime)
    (hp2 : p ≠ 2) (x : Fin k → ZMod (p ^ r))
    (h : 2 ≤ (Finset.univ.filter fun i => Nat.Coprime (x i).val p).card) :
    IsWeightedZeroSum (p ^ r) k (unitSet (p ^ r)) x
Sources
  • Santanu Mondal, Krishnendu Paul and Shameek Paul, Zero-Sum Constants Related to the Jacobi Symbol, Journal of Integer Sequences 27 (2024), Article 24.1.7, Lemma 16 (jis-2024-24.1.7-lem-16).

TheoremThree-term sums of square-weighted units cover \(\mathbb{Z}_{p^r}\)#●ready to prove

Let \(p \ge 7\) be a prime, \(r\) a natural number and \(n = p^r\); write \(\mathbb{Z}_n = \mathbb{Z}/n\mathbb{Z}\) and \(A = U(n)^2\) for the set of squares of units of \(\mathbb{Z}_n\). For all units \(x_1, x_2, x_3\) of \(\mathbb{Z}_n\), \(A x_1 + A x_2 + A x_3 = \mathbb{Z}_n\): every \(z \in \mathbb{Z}_n\) equals \(a_1 x_1 + a_2 x_2 + a_3 x_3\) for some \(a_1, a_2, a_3 \in A\).

public theorem_wanted unit_square_three_sumset_eq_univ (p r : ℕ) (hp : p.Prime) (h7 : 7 ≤ p)
    (x : Fin 3 → ZMod (p ^ r)) (hx : ∀ i, IsUnit (x i)) (z : ZMod (p ^ r)) :
    ∃ a : Fin 3 → ZMod (p ^ r), (∀ i, a i ∈ unitSqSet (p ^ r)) ∧ ∑ i, a i * x i = z
Sources
  • Santanu Mondal, Krishnendu Paul and Shameek Paul, Zero-Sum Constants Related to the Jacobi Symbol, Journal of Integer Sequences 27 (2024), Article 24.1.7, Lemma 17 (jis-2024-24.1.7-lem-17).
20 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.