The one-term zero sequence has a square-weighted zero sum to Square-weighted constants of nonsquares with even \(2\)-adic valuation

TheoremThe one-term zero sequence has a square-weighted zero sum#✓fully proved

Let \(n \ge 2\) and let \(S(n)\) be the set of nonzero squares in \(\mathbb{Z}_n\). The sequence over \(\mathbb{Z}_n\) whose only term is \(0\) has an \(S(n)\)-weighted zero sum: there is a weight \(a \in S(n)\) with \(a \cdot 0 = 0\).

The weight \(a = 1\) works; it lies in \(S(n)\) because \(1 \ne 0\) in \(\mathbb{Z}_n\) when \(n \ge 2\).

public theorem zeroSingleton_hasWeightedZeroSum (n : ℕ) (hn : 2 ≤ n) :
    HasWeightedZeroSum (squareSet n) (fun _ : Fin 1 => 0)

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Introduction.

Uses 2

Statement usesWeighted zero-sum sequences · Nonzero squares modulo \(n\)

TheoremDecomposition of the nonzero squares modulo a prime power#●ready to prove

Let \(p\) be a prime, let \(r \ge 1\), and let \(l = \lfloor (r - 1)/2 \rfloor\). Write \(S(p^r)\) for the set of nonzero squares in \(\mathbb{Z}_{p^r}\), \(U(p^r)^2\) for the set of squares of units in \(\mathbb{Z}_{p^r}\), and \(p^{2k} U(p^r)^2 = \{p^{2k} x : x \in U(p^r)^2\}\). Then

\[S(p^r) = \bigcup_{k=0}^{l} p^{2k} U(p^r)^2,\]

and the sets \(p^{2k} U(p^r)^2\) for \(k = 0, \dots, l\) are pairwise disjoint.

public theorem_wanted squareSet_primePower_decomposition (p r : ℕ) (hp : p.Prime) (hr : 0 < r) :
    let l := (r - 1) / 2
    let pieces : Fin (l + 1) → Set (ZMod (p ^ r)) := fun k =>
      ((p : ZMod (p ^ r)) ^ (2 * (k : ℕ))) • unitSquareSet (p ^ r)
    squareSet (p ^ r) = ⋃ k, pieces k ∧ Set.PairwiseDisjoint Set.univ pieces

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Lemma 4.

Uses 2

Statement usesNonzero squares modulo \(n\) · Squares of units modulo n

TheoremScaled unit squares modulo a prime power#●ready to prove

Let \(p\) be a prime and \(r, k\) natural numbers with \(k = 0\) or \(2k < r\), and write \(U(m)^2\) for the set of squares of units of \(\mathbb{Z}/m\mathbb{Z}\). Then the set \(p^{2k} U(p^r)^2 = \{p^{2k} x : x \in U(p^r)^2\}\) in \(\mathbb{Z}/p^r\mathbb{Z}\) has the same number of elements as \(U(p^{r-2k})^2\).

public theorem_wanted ncard_scale_unitSquares_primePower (p r k : ℕ) (hp : p.Prime)
    (hk : k ≤ (r - 1) / 2) :
    (((p : ZMod (p ^ r)) ^ (2 * k)) • unitSquareSet (p ^ r)).ncard =
      (unitSquareSet (p ^ (r - 2 * k))).ncard

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Lemma 5.

Uses 1

Statement usesSquares of units modulo n

TheoremNumber of nonzero squares modulo a prime power#●ready to prove

Let \(p\) be a prime and \(r \ge 1\), and write \(S(m)\) for the set of nonzero squares and \(U(m)^2\) for the set of squares of units in \(\mathbb{Z}/m\mathbb{Z}\). If \(r\) is even, then \(|S(p^r)| = \sum_{k=0}^{r/2-1} |U(p^{r-2k})^2|\), and if \(r\) is odd, then \(|S(p^r)| = \sum_{k=0}^{(r-1)/2} |U(p^{r-2k})^2|\).

public theorem_wanted ncard_squareSet_primePower (p r : ℕ) (hp : p.Prime) (hr : 0 < r) :
    (Even r → (squareSet (p ^ r)).ncard =
      ∑ k ∈ Finset.range (r / 2), (unitSquareSet (p ^ (r - 2 * k))).ncard) ∧
    (Odd r → (squareSet (p ^ r)).ncard =
      ∑ k ∈ Finset.range ((r + 1) / 2), (unitSquareSet (p ^ (r - 2 * k))).ncard)

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Theorem 6.

Uses 2

Statement usesNonzero squares modulo \(n\) · Squares of units modulo n

TheoremSquare-weighted zero sums lift from a prime-power component#●ready to prove

Let \(n \ge 2\), let \(p\) be a prime dividing \(n\), and let \(r\) be the exponent of \(p\) in \(n\). Write \(S(m)\) for the set of nonzero squares in \(\mathbb{Z}_m\). Let \(x_1, \dots, x_k\) be a sequence in \(\mathbb{Z}_n\) whose reduction \(\bar x_1, \dots, \bar x_k\) modulo \(p^r\) has an \(S(p^r)\)-weighted zero sum, that is, there are \(b_1, \dots, b_k \in S(p^r)\) with \(\sum_i b_i \bar x_i = 0\). Then there are \(a_1, \dots, a_k \in S(n)\) with \(\sum_i a_i x_i = 0\).

public theorem_wanted squareWeightedZeroSum_of_primePower_reduction (n p r k : ℕ)
    (hn : 2 ≤ n) (hp : p.Prime) (hpn : p ∣ n) (hval : n.factorization p = r)
    (S : Fin k → ZMod n)
    (hS : HasWeightedZeroSum (squareSet (p ^ r))
      (fun i => (ZMod.cast (S i) : ZMod (p ^ r)))) :
    HasWeightedZeroSum (squareSet n) S

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Lemma 7.

Uses 2

Statement usesWeighted zero-sum sequences · Nonzero squares modulo \(n\)

TheoremPrime-power bound for the square-weighted consecutive constant#●ready to prove

Let \(n \ge 2\), let \(p\) be a prime dividing \(n\) and let \(r = v_p(n)\) be the exponent of \(p\) in \(n\). For a natural number \(m\), write \(S(m)\) for the set of nonzero squares in \(\mathbb{Z}_m = \mathbb{Z}/m\mathbb{Z}\) and \(C_{S(m)}\) for the \(S(m)\)-weighted consecutive constant of \(\mathbb{Z}_m\). Then \(C_{S(n)} \le C_{S(p^r)}\).

public theorem_wanted weightedConsecutiveConstant_squareSet_le_primePower (n p r : ℕ)
    (hn : 2 ≤ n) (hp : p.Prime) (hpn : p ∣ n) (hval : n.factorization p = r) :
    weightedConsecutiveConstant n (squareSet n) ≤
      weightedConsecutiveConstant (p ^ r) (squareSet (p ^ r))

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Corollary 8.

Uses 2

Statement usesNonzero squares modulo \(n\) · Weighted consecutive zero-sum constant

TheoremSquare-weighted zero sums lift from \(p\) to odd powers \(p^r\)#●ready to prove

Let \(p \ge 2\) be a natural number and \(r\) an odd natural number. Write \(S(m)\) for the set of nonzero squares in \(\mathbb{Z}_m\). Let \(x_1, \dots, x_k\) be a sequence in \(\mathbb{Z}_{p^r}\) whose reduction \(\bar x_1, \dots, \bar x_k\) modulo \(p\) has an \(S(p)\)-weighted zero sum, that is, there are \(b_1, \dots, b_k \in S(p)\) with \(\sum_i b_i \bar x_i = 0\). Then there are \(a_1, \dots, a_k \in S(p^r)\) with \(\sum_i a_i x_i = 0\).

This is at least as strong as the reading with weights in \(U(p)^2\), the squares of units of \(\mathbb{Z}_p\), because \(U(p)^2 \subseteq S(p)\); the two agree for prime \(p\).

public theorem_wanted squareWeightedZeroSum_of_reduction_oddPower (p r k : ℕ)
    (hp : 2 ≤ p) (hr : Odd r) (T : Fin k → ZMod (p ^ r))
    (hT : HasWeightedZeroSum (squareSet p) (fun i => (ZMod.cast (T i) : ZMod p))) :
    HasWeightedZeroSum (squareSet (p ^ r)) T

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Lemma 9.

Uses 2

Statement usesWeighted zero-sum sequences · Nonzero squares modulo \(n\)

TheoremSquare-weighted zero-sum free unit triples modulo even powers of two#●ready to prove

Let \(r\) be a nonzero even natural number, and let \(x_1, x_2, x_3\) be units of \(\mathbb{Z}_{2^r}\) that are each congruent to \(1\) modulo \(4\). Write \(S(2^r)\) for the set of nonzero squares in \(\mathbb{Z}_{2^r}\). Then \((x_1, x_2, x_3)\) has no \(S(2^r)\)-weighted zero-sum subsequence: there are no non-empty set \(J\) of indices and weights \(a_j \in S(2^r)\) for \(j \in J\) with \(\sum_{j \in J} a_j x_j = 0\).

public theorem_wanted no_squareWeightedSubseq_three_units_twoPower (r : ℕ)
    (hr0 : r ≠ 0) (hrEven : Even r) (S : Fin 3 → ZMod (2 ^ r))
    (hunit : ∀ i, IsUnit (S i))
    (hred : ∀ i, (ZMod.cast (S i) : ZMod 4) = 1) :
    ¬HasWeightedZeroSumSubseq (squareSet (2 ^ r)) S

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Lemma 10.

Uses 2

Statement usesWeighted zero-sum subsequences · Nonzero squares modulo \(n\)

TheoremThree-term sequences without square-weighted zero-sum subsequences#●ready to prove

Let \(p\) be a prime and \(r\) a nonzero even natural number, and write \(S(m)\) for the set of nonzero squares in \(\mathbb{Z}/m\mathbb{Z}\). Let \(z_1, z_2\) be units of \(\mathbb{Z}/p^2\mathbb{Z}\) whose reduction \((z_1 \bmod p, z_2 \bmod p)\) is not an \(S(p)\)-weighted zero-sum sequence. Let \(T = (x_1, x_2, y_1)\) be a sequence in \(\mathbb{Z}/p^r\mathbb{Z}\) whose reduction modulo \(p^2\) is \((z_1, z_2, p)\). Then \(T\) has no \(S(p^r)\)-weighted zero-sum subsequence.

The paper states the lemma for sequences of units modulo \(p^r\), which no \(y_1\) reducing to the nonunit \(p\) can be; following the paper's proof and its application in Theorem 12, the sequence is taken in \(\mathbb{Z}/p^r\mathbb{Z}\). Then \(x_1, x_2\) are automatically units, since \(z_1, z_2\) are.

public theorem_wanted no_squareWeightedSubseq_pair_and_prime_of_reduction (p r : ℕ)
    (hp : p.Prime) (hr0 : r ≠ 0) (hrEven : Even r) (z : Fin 2 → ZMod (p ^ 2))
    (hz : ∀ i, IsUnit (z i))
    (hzred : ¬HasWeightedZeroSum (squareSet p) (fun i => (ZMod.cast (z i) : ZMod p)))
    (S : Fin 3 → ZMod (p ^ r))
    (hS : ∀ i, (ZMod.cast (S i) : ZMod (p ^ 2)) = ![z 0, z 1, (p : ZMod (p ^ 2))] i) :
    ¬HasWeightedZeroSumSubseq (squareSet (p ^ r)) S

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Lemma 11.

Uses 3

Statement usesWeighted zero-sum sequences · Weighted zero-sum subsequences · Nonzero squares modulo \(n\)

TheoremSquare-weighted Davenport constant of even squares is at least four#●ready to prove

Let \(n \ge 2\) be an even perfect square. Write \(S(n)\) for the set of nonzero squares in \(\mathbb{Z}_n = \mathbb{Z}/n\mathbb{Z}\) and \(D_{S(n)} \in \mathbb{N} \cup \{\infty\}\) for the weighted Davenport constant of \(\mathbb{Z}_n\) with weight set \(S(n)\), a weight acting by multiplication. Then \(D_{S(n)} \ge 4\).

public theorem_wanted weightedDavenport_squareSet_evenSquare_lowerBound (n : ℕ)
    (hn : 2 ≤ n) (heven : Even n) (hsquare : IsSquare n) :
    4 ≤ weightedDavenport (zmodWeightReps (squareSet n)) (ZMod n)

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Theorem 12.

Uses 3

Statement usesNonzero squares modulo \(n\) · Weighted Davenport constant · Representatives of a set of residues

TheoremLifting weighted zero sums from p² to an even power of p#●ready to prove

Let \(p \ge 2\), \(r \ne 0\) and \(k\) be natural numbers with \(r\) even, and let \(t_1, \dots, t_k\) be elements of \(\mathbb{Z}/p^r\mathbb{Z}\), with reductions \(\bar t_1, \dots, \bar t_k\) modulo \(p^2\). Write \(U(p^2)^2\) for the set of squares of units of \(\mathbb{Z}/p^2\mathbb{Z}\) and \(S(p^r)\) for the set of nonzero squares of \(\mathbb{Z}/p^r\mathbb{Z}\). If there are \(a_1, \dots, a_k \in U(p^2)^2\) with \(a_1 \bar t_1 + \dots + a_k \bar t_k = 0\) in \(\mathbb{Z}/p^2\mathbb{Z}\), then there are \(b_1, \dots, b_k \in S(p^r)\) with \(b_1 t_1 + \dots + b_k t_k = 0\) in \(\mathbb{Z}/p^r\mathbb{Z}\).

The paper states the lemma for \(p > 0\); the stronger hypothesis \(p \ge 2\) is deliberate.

public theorem_wanted squareWeightedZeroSum_of_reduction_square (p r k : ℕ)
    (hp : 2 ≤ p) (hr0 : r ≠ 0) (hrEven : Even r)
    (T : Fin k → ZMod (p ^ r))
    (hT : HasWeightedZeroSum (unitSquareSet (p ^ 2))
      (fun i => (ZMod.cast (T i) : ZMod (p ^ 2)))) :
    HasWeightedZeroSum (squareSet (p ^ r)) T

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Lemma 13.

Uses 3

Statement usesWeighted zero-sum sequences · Nonzero squares modulo \(n\) · Squares of units modulo n

TheoremSquare-weighted constants modulo \(p^r\), for \(p \ge 2\) and nonzero even \(r\), are at most unit-square constants modulo \(p^2\)#●ready to prove

Square-weighted constants modulo \(p^r\), for \(p \ge 2\) and nonzero even \(r\), are at most unit-square constants modulo \(p^2\). Let \(p \ge 2\) be a natural number and let \(r\) be a nonzero even natural number. Write \(S(p^r)\) for the set of nonzero squares in \(\mathbb{Z}_{p^r}\) and \(U(p^2)^2\) for the set of squares of units in \(\mathbb{Z}_{p^2}\). For a weight set \(A \subseteq \mathbb{Z}_m\), write \(D_A(\mathbb{Z}_m)\) for the \(A\)-weighted Davenport constant of \(\mathbb{Z}_m\), where \(A\) acts through its representatives in \(\{0, \dots, m - 1\}\) and the value lies in \(\mathbb{N} \cup \{\infty\}\), and write \(C_A\) for the least positive length \(k\) such that every sequence of length \(k\) in \(\mathbb{Z}_m\) has a non-empty consecutive \(A\)-weighted zero-sum subsequence, or \(0\) if there is no such length. Then \(D_{S(p^r)}(\mathbb{Z}_{p^r}) \le D_{U(p^2)^2}(\mathbb{Z}_{p^2})\) and \(C_{S(p^r)} \le C_{U(p^2)^2}\), the first constant in each inequality taken in \(\mathbb{Z}_{p^r}\) and the second in \(\mathbb{Z}_{p^2}\).

The paper says \(p\) positive; \(p = 1\) is excluded (the paper assumes throughout that the modulus is at least \(2\)), since then \(S(1)\) is empty, so \(D_{S(1)}(\mathbb{Z}_1) = \infty\), while \(D_{U(1)^2}(\mathbb{Z}_1) = 1\).

public theorem_wanted squareSet_constants_le_unitSquares_modSquare (p r : ℕ)
    (hp : 2 ≤ p) (hr0 : r ≠ 0) (hrEven : Even r) :
    weightedDavenport (zmodWeightReps (squareSet (p ^ r))) (ZMod (p ^ r)) ≤
        weightedDavenport (zmodWeightReps (unitSquareSet (p ^ 2))) (ZMod (p ^ 2)) ∧
      weightedConsecutiveConstant (p ^ r) (squareSet (p ^ r)) ≤
        weightedConsecutiveConstant (p ^ 2) (unitSquareSet (p ^ 2))

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Corollary 14.

Uses 5

Statement usesNonzero squares modulo \(n\) · Squares of units modulo n · Weighted consecutive zero-sum constant · Weighted Davenport constant · Representatives of a set of residues

TheoremConsecutive square-weighted constant of an even power of two is at most four#●ready to prove

For every even natural number \(r \ne 0\), the consecutive \(S(2^r)\)-weighted zero-sum constant satisfies \(C_{S(2^r)} \le 4\), where \(S(2^r)\) is the set of nonzero squares of \(\mathbb{Z}/2^r\mathbb{Z}\).

public theorem_wanted weightedConsecutiveConstant_squareSet_twoPower_le_four (r : ℕ)
    (hr0 : r ≠ 0) (hrEven : Even r) :
    weightedConsecutiveConstant (2 ^ r) (squareSet (2 ^ r)) ≤ 4

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Theorem 15.

Uses 2

Statement usesNonzero squares modulo \(n\) · Weighted consecutive zero-sum constant

TheoremSquare-weighted constants of even squares#●ready to prove

Let \(n \ge 2\) be an even perfect square and let \(S(n)\) be the set of nonzero squares in \(\mathbb{Z}_n\). Then the \(S(n)\)-weighted Davenport constant of \(\mathbb{Z}_n\), with weights the representatives in \(\{0, \dots, n - 1\}\) of the elements of \(S(n)\), equals \(4\). Moreover, some positive length \(k\) forces every sequence of length \(k\) in \(\mathbb{Z}_n\) to have a non-empty consecutive \(S(n)\)-weighted zero-sum subsequence, and the least such length, the consecutive constant \(C_{S(n)}\), equals \(4\).

Since the infimum of the empty set of natural numbers is \(0\), the existence clause makes the equality \(C_{S(n)} = 4\) nonvacuous.

public theorem_wanted squareSet_constants_evenSquare (n : ℕ) (hn : 2 ≤ n)
    (heven : Even n) (hsquare : IsSquare n) :
    (weightedConsecutiveDefiningSet n (squareSet n)).Nonempty ∧
      weightedDavenport (zmodWeightReps (squareSet n)) (ZMod n) = 4 ∧
      weightedConsecutiveConstant n (squareSet n) = 4

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Corollary 16.

Uses 5

Statement usesNonzero squares modulo \(n\) · Weighted consecutive zero-sum constant · Lengths forcing a consecutive weighted zero sum · Weighted Davenport constant · Representatives of a set of residues

TheoremTwo units without square-weighted zero sums modulo any prime divisor#●ready to prove

Let \(n \ge 2\) be odd, and write \(S(m)\) for the set of nonzero squares in \(\mathbb{Z}/m\mathbb{Z}\). Then there are units \(u, v\) of \(\mathbb{Z}/n\mathbb{Z}\) such that for every prime \(p\) dividing \(n\), the sequence \((u \bmod p, v \bmod p)\) in \(\mathbb{Z}/p\mathbb{Z}\) has no \(S(p)\)-weighted zero-sum subsequence.

public theorem_wanted exists_pair_units_avoiding_prime_squareWeights (n : ℕ)
    (hn : 2 ≤ n) (hnOdd : Odd n) :
    ∃ u v : ZMod n, IsUnit u ∧ IsUnit v ∧
      ∀ p : ℕ, p.Prime → p ∣ n →
        ¬HasWeightedZeroSumSubseq (squareSet p)
          (fun i : Fin 2 => (ZMod.cast (![u, v] i) : ZMod p))

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Proposition 17.

Uses 2

Statement usesWeighted zero-sum subsequences · Nonzero squares modulo \(n\)

TheoremSquare-weighted zero-sum free unit pairs lift to odd prime powers#●ready to prove

Let \(p\) be an odd prime, let \(r \ge 1\), and let \(x_1, x_2\) be units of \(\mathbb{Z}_{p^r}\). Write \(S(m)\) for the set of nonzero squares in \(\mathbb{Z}_m\), and say that a sequence \((y_i)\) in \(\mathbb{Z}_m\) has an \(A\)-weighted zero-sum subsequence when there are a non-empty set \(J\) of indices and weights \(a_j \in A\) for \(j \in J\) with \(\sum_{j \in J} a_j y_j = 0\). If the reduction \((\bar x_1, \bar x_2)\) of \((x_1, x_2)\) modulo \(p\) has no \(S(p)\)-weighted zero-sum subsequence, then \((x_1, x_2)\) has no \(S(p^r)\)-weighted zero-sum subsequence.

The paper states the hypothesis with \(Q_p\), the set of nonzero quadratic residues modulo \(p\), which equals \(S(p)\).

public theorem_wanted no_squareWeightedSubseq_pair_of_reduction (p r : ℕ)
    (hp : p.Prime) (hpOdd : Odd p) (hr : 0 < r) (S : Fin 2 → ZMod (p ^ r))
    (hunit : ∀ i, IsUnit (S i))
    (hred : ¬HasWeightedZeroSumSubseq (squareSet p)
      (fun i => (ZMod.cast (S i) : ZMod p))) :
    ¬HasWeightedZeroSumSubseq (squareSet (p ^ r)) S

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Lemma 18.

Uses 2

Statement usesWeighted zero-sum subsequences · Nonzero squares modulo \(n\)

TheoremThe square-weighted Davenport constant of an odd modulus is at least three#●ready to prove

Let \(n \ge 2\) be odd, let \(S(n)\) be the set of nonzero squares in \(\mathbb{Z}_n\), and let \(A\) be the set of integers \(a\) with \(0 \le a < n\) whose residue modulo \(n\) lies in \(S(n)\). Then the \(A\)-weighted Davenport constant \(D_{S(n)}\) of \(\mathbb{Z}_n\) is at least \(3\).

public theorem_wanted weightedDavenport_squareSet_odd_lowerBound (n : ℕ)
    (hn : 2 ≤ n) (hnOdd : Odd n) :
    3 ≤ weightedDavenport (zmodWeightReps (squareSet n)) (ZMod n)

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Theorem 19.

Uses 3

Statement usesNonzero squares modulo \(n\) · Weighted Davenport constant · Representatives of a set of residues

TheoremSquare-weighted Davenport constant for an even 2-adic valuation of at least two#●ready to prove

Let \(n \ge 2\) be a natural number whose exponent \(v_2(n)\) of \(2\) is even and at least \(2\). Write \(S(n)\) for the set of nonzero squares in \(\mathbb{Z}_n = \mathbb{Z}/n\mathbb{Z}\) and \(D_{S(n)} \in \mathbb{N} \cup \{\infty\}\) for the weighted Davenport constant of \(\mathbb{Z}_n\) with weight set \(S(n)\), a weight acting by multiplication. Then \(D_{S(n)} \ge 3\).

public theorem_wanted weightedDavenport_squareSet_even_twoValuation_lowerBound (n : ℕ)
    (hn : 2 ≤ n) (hvalEven : Even (n.factorization 2))
    (hval : 2 ≤ n.factorization 2) :
    3 ≤ weightedDavenport (zmodWeightReps (squareSet n)) (ZMod n)

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Theorem 20.

Uses 3

Statement usesNonzero squares modulo \(n\) · Weighted Davenport constant · Representatives of a set of residues

TheoremConsecutive square-weighted constant of an odd prime to an odd power is at most three#●ready to prove

For every odd prime \(p\) and every odd natural number \(r\), the consecutive \(S(p^r)\)-weighted zero-sum constant satisfies \(C_{S(p^r)} \le 3\), where \(S(p^r)\) is the set of nonzero squares of \(\mathbb{Z}/p^r\mathbb{Z}\).

public theorem_wanted weightedConsecutiveConstant_squareSet_oddPrimePower_le_three
    (p r : ℕ) (hp : p.Prime) (hpOdd : Odd p) (hrOdd : Odd r) :
    weightedConsecutiveConstant (p ^ r) (squareSet (p ^ r)) ≤ 3

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Theorem 21.

Uses 2

Statement usesNonzero squares modulo \(n\) · Weighted consecutive zero-sum constant

TheoremSquare-weighted constants of nonsquares with even \(2\)-adic valuation#●ready to prove

Let \(n \ge 2\) be a natural number that is not a perfect square and whose \(2\)-adic valuation \(v_2(n)\) is even (possibly zero), and let \(S(n)\) be the set of nonzero squares in \(\mathbb{Z}_n\). Then the \(S(n)\)-weighted Davenport constant of \(\mathbb{Z}_n\), with weights the representatives in \(\{0, \dots, n - 1\}\) of the elements of \(S(n)\), equals \(3\). Moreover, some positive length \(k\) forces every sequence of length \(k\) in \(\mathbb{Z}_n\) to have a non-empty consecutive \(S(n)\)-weighted zero-sum subsequence, and the least such length, the consecutive constant \(C_{S(n)}\), equals \(3\).

public theorem_wanted squareSet_constants_nonsquare_even_twoValuation (n : ℕ)
    (hn : 2 ≤ n) (hnotSquare : ¬IsSquare n)
    (hvalEven : Even (n.factorization 2)) :
    (weightedConsecutiveDefiningSet n (squareSet n)).Nonempty ∧
      weightedDavenport (zmodWeightReps (squareSet n)) (ZMod n) = 3 ∧
      weightedConsecutiveConstant n (squareSet n) = 3

Sources

• Krishnendu Paul and Shameek Paul, Square-Weighted Zero-Sum Constants, Journal of Integer Sequences 27 (2024), Article 24.6.6, Corollary 22.

Uses 5

Statement usesNonzero squares modulo \(n\) · Weighted consecutive zero-sum constant · Lengths forcing a consecutive weighted zero sum · Weighted Davenport constant · Representatives of a set of residues

1 fully proved19 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.