Consecutive square-weighted constant of an odd power of two is at most two to A nested ceiling identity for divisors

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

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

public theorem_wanted weightedConsecutiveConstant_squareSet_odd_twoPower_le_two (r : ℕ)
    (hrOdd : Odd r) :
    weightedConsecutiveConstant (2 ^ r) (squareSet (2 ^ r)) ≤ 2

Sources

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

Uses 2

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

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

Let \(n\) be a positive even natural number whose \(2\)-adic valuation \(v_2(n)\) is odd, 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 \(2\). 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 \(2\).

public theorem_wanted squareSet_constants_odd_twoValuation (n : ℕ) (hn : 0 < n)
    (hnEven : Even n) (hvalOdd : Odd (n.factorization 2)) :
    (weightedConsecutiveDefiningSet n (squareSet n)).Nonempty ∧
      weightedDavenport (zmodWeightReps (squareSet n)) (ZMod n) = 2 ∧
      weightedConsecutiveConstant n (squareSet n) = 2

Sources

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

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

TheoremFour-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 \(w_1, w_2, u\) be units of \(\mathbb{Z}/p^r\mathbb{Z}\) such that the reduction \((w_1 \bmod p, w_2 \bmod p)\) has no \(S(p)\)-weighted zero-sum subsequence. Then the sequence \((u w_1, u w_2, p w_1, p w_2)\) in \(\mathbb{Z}/p^r\mathbb{Z}\) has no \(S(p^r)\)-weighted zero-sum subsequence.

public theorem_wanted no_squareWeightedSubseq_fourTerm_pattern (p r : ℕ)
    (hp : p.Prime) (hr0 : r ≠ 0) (hrEven : Even r)
    (w₁ w₂ u : ZMod (p ^ r)) (hw₁ : IsUnit w₁) (hw₂ : IsUnit w₂)
    (hu : IsUnit u)
    (hred : ¬HasWeightedZeroSumSubseq (squareSet p)
      (fun i : Fin 2 => (ZMod.cast (![w₁, w₂] i) : ZMod p))) :
    ¬HasWeightedZeroSumSubseq (squareSet (p ^ r))
      ![u * w₁, u * w₂, (p : ZMod (p ^ r)) * w₁, (p : ZMod (p ^ r)) * w₂]

Sources

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

Uses 2

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

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

Let \(n \ge 2\) be an odd perfect square, 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 \(5\).

public theorem_wanted weightedDavenport_squareSet_oddSquare_lowerBound (n : ℕ)
    (hn : 2 ≤ n) (hnOdd : Odd n) (hsquare : IsSquare n) :
    5 ≤ 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 26.

Uses 3

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

TheoremThree unit-square cosets sum to every residue modulo an odd prime power#●ready to prove

Let \(p\) be an odd prime, let \(r \ge 1\), and let \(A = U(p^r)^2\) be the set of squares of units of \(\mathbb{Z}/p^r\mathbb{Z}\); for \(y \in \mathbb{Z}/p^r\mathbb{Z}\) write \(Ay = \{ay : a \in A\}\). For all units \(y_1, y_2, y_3\) of \(\mathbb{Z}/p^r\mathbb{Z}\), every element of \(\mathbb{Z}/p^r\mathbb{Z}\) is a sum \(x_1 + x_2 + x_3\) with \(x_1 \in Ay_1\), \(x_2 \in Ay_2 \cup \{0\}\) and \(x_3 \in Ay_3 \cup \{0\}\).

public theorem_wanted three_unitSquare_cosets_cover (p r : ℕ) (hp : p.Prime)
    (hpOdd : Odd p) (hr : 0 < r) (y₁ y₂ y₃ : ZMod (p ^ r))
    (hy₁ : IsUnit y₁) (hy₂ : IsUnit y₂) (hy₃ : IsUnit y₃) :
    unitSquareSet (p ^ r) * {y₁} +
      (unitSquareSet (p ^ r) * {y₂} ∪ {0} + (unitSquareSet (p ^ r) * {y₃} ∪ {0})) =
        Set.univ

Sources

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

Uses 1

Statement usesSquares of units modulo n

TheoremThe square-weighted Davenport constant of an even power of an odd prime is at most five#●ready to prove

Let \(p\) be an odd prime, let \(r\) be a nonzero even natural number, let \(S(p^r)\) be the set of nonzero squares in \(\mathbb{Z}_{p^r}\), and let \(A\) be the set of integers \(a\) with \(0 \le a < p^r\) whose residue modulo \(p^r\) lies in \(S(p^r)\). Then the \(A\)-weighted Davenport constant \(D_{S(p^r)}\) of \(\mathbb{Z}_{p^r}\) is at most \(5\).

public theorem_wanted weightedDavenport_squareSet_oddPrimePower_le_five (p r : ℕ)
    (hp : p.Prime) (hpOdd : Odd p) (hr0 : r ≠ 0) (hrEven : Even r) :
    weightedDavenport (zmodWeightReps (squareSet (p ^ r))) (ZMod (p ^ r)) ≤ 5

Sources

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

Uses 3

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

TheoremThe square-weighted Davenport constant of an odd square is five#●ready to prove

Let \(n \ge 2\) be an odd perfect square, 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\) equals \(5\).

public theorem_wanted weightedDavenport_squareSet_oddSquare (n : ℕ) (hn : 2 ≤ n)
    (hnOdd : Odd n) (hsquare : IsSquare n) :
    weightedDavenport (zmodWeightReps (squareSet n)) (ZMod n) = 5

Sources

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

Uses 3

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

TheoremUnit-square-weighted consecutive constant modulo 25 equals nine#●ready to prove

Let \(U(25)^2\) be the set of squares of units of \(\mathbb{Z}_{25} = \mathbb{Z}/25\mathbb{Z}\). Some positive length \(k\) has the property that every sequence of \(k\) elements of \(\mathbb{Z}_{25}\) has a nonempty block of consecutive terms with a \(U(25)^2\)-weighted sum equal to zero, and the least such length, the \(U(25)^2\)-weighted consecutive constant \(C_{U(25)^2}\) of \(\mathbb{Z}_{25}\), equals \(9\).

public theorem_wanted weightedConsecutiveConstant_unitSquares_twentyFive :
    (weightedConsecutiveDefiningSet 25 (unitSquareSet 25)).Nonempty ∧
      weightedConsecutiveConstant 25 (unitSquareSet 25) = 9

Sources

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

Uses 3

Statement usesSquares of units modulo n · Weighted consecutive zero-sum constant · Lengths forcing a consecutive weighted zero sum

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

For every odd natural number \(n \ge 2\) that is a perfect square, the consecutive \(S(n)\)-weighted zero-sum constant satisfies \(C_{S(n)} \le 9\), where \(S(n)\) is the set of nonzero squares of \(\mathbb{Z}/n\mathbb{Z}\).

The hypothesis \(n \ge 2\) is the paper's standing convention.

public theorem_wanted weightedConsecutiveConstant_squareSet_oddSquare_le_nine (n : ℕ)
    (hn : 2 ≤ n) (hnOdd : Odd n) (hsquare : IsSquare n) :
    weightedConsecutiveConstant n (squareSet n) ≤ 9

Sources

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

Uses 2

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

TheoremSquare-weighted consecutive constant of \(p^r\) for prime \(p \ge 7\) and even \(r \ge 4\) is at most five#●ready to prove

Square-weighted consecutive constant of \(p^r\) for prime \(p \ge 7\) and even \(r \ge 4\) is at most five. Let \(p \ge 7\) be a prime and \(r \ge 4\) an even natural number. Write \(S(p^r)\) for the set of nonzero squares in \(\mathbb{Z}_{p^r} = \mathbb{Z}/p^r\mathbb{Z}\) and \(C_{S(p^r)}\) for the \(S(p^r)\)-weighted consecutive constant of \(\mathbb{Z}_{p^r}\). Then \(C_{S(p^r)} \le 5\).

public theorem_wanted weightedConsecutiveConstant_squareSet_largePrimePower_le_five
    (p r : ℕ) (hp : p.Prime) (hpSeven : 7 ≤ p) (hrEven : Even r)
    (hrFour : 4 ≤ r) :
    weightedConsecutiveConstant (p ^ r) (squareSet (p ^ r)) ≤ 5

Sources

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

Uses 2

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

TheoremSquare-weighted consecutive constant five for odd squares with a large prime fourth power#●ready to prove

Let \(n \ge 2\) be an odd perfect square and let \(p \ge 7\) be a prime with \(p^4 \mid n\). Write \(S(n)\) for the set of nonzero squares in \(\mathbb{Z}_n = \mathbb{Z}/n\mathbb{Z}\). Then some positive length \(k\) has the property that every sequence of \(k\) elements of \(\mathbb{Z}_n\) has a nonempty block of consecutive terms with an \(S(n)\)-weighted sum equal to zero, and the least such length, the \(S(n)\)-weighted consecutive constant \(C_{S(n)}\) of \(\mathbb{Z}_n\), equals \(5\).

public theorem_wanted weightedConsecutiveConstant_squareSet_oddSquare_largePrime (n p : ℕ)
    (hn : 2 ≤ n) (hnOdd : Odd n) (hnSquare : IsSquare n)
    (hp : p.Prime) (hpSeven : 7 ≤ p) (hdiv : p ^ 4 ∣ n) :
    (weightedConsecutiveDefiningSet n (squareSet n)).Nonempty ∧
      weightedConsecutiveConstant n (squareSet n) = 5

Sources

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

Uses 3

Statement usesNonzero squares modulo \(n\) · Weighted consecutive zero-sum constant · Lengths forcing a consecutive weighted zero sum

TheoremFour unit terms force a unit-square-weighted zero sum modulo a power of 5#●ready to prove

Let \(r \ge 1\) and let \(U(5^r)^2\) be the set of squares of units of \(\mathbb{Z}/5^r\mathbb{Z}\). If a sequence \(s_1, \dots, s_k\) in \(\mathbb{Z}/5^r\mathbb{Z}\) has at least four terms, at distinct positions, that are units, then there are \(a_1, \dots, a_k \in U(5^r)^2\) with \(a_1 s_1 + \dots + a_k s_k = 0\).

public theorem_wanted unitSquareWeightedZeroSum_modFivePower_of_four_units (r k : ℕ)
    (hr : 0 < r) (S : Fin k → ZMod (5 ^ r))
    (hunits : ∃ J : Finset (Fin k), 4 ≤ J.card ∧ ∀ i ∈ J, IsUnit (S i)) :
    HasWeightedZeroSum (unitSquareSet (5 ^ r)) S

Sources

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

Uses 2

Statement usesWeighted zero-sum sequences · Squares of units modulo n

TheoremSquare-weighted consecutive constant of \(5^r\) for even \(r \ge 4\) is at most seven#●ready to prove

Let \(r \ge 4\) be an even natural number. Write \(S(5^r)\) for the set of nonzero squares in \(\mathbb{Z}_{5^r} = \mathbb{Z}/5^r\mathbb{Z}\) and \(C_{S(5^r)}\) for the \(S(5^r)\)-weighted consecutive constant of \(\mathbb{Z}_{5^r}\). Then \(C_{S(5^r)} \le 7\).

public theorem_wanted weightedConsecutiveConstant_squareSet_fivePower_le_seven (r : ℕ)
    (hrEven : Even r) (hrFour : 4 ≤ r) :
    weightedConsecutiveConstant (5 ^ r) (squareSet (5 ^ r)) ≤ 7

Sources

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

Uses 2

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

TheoremSquare-weighted consecutive constant of squares divisible by 625 is at most seven#●ready to prove

Let \(n \ge 2\) be a perfect square with \(5^4 \mid n\). Write \(S(n)\) for the set of nonzero squares in \(\mathbb{Z}_n = \mathbb{Z}/n\mathbb{Z}\) and \(C_{S(n)}\) for the \(S(n)\)-weighted consecutive constant of \(\mathbb{Z}_n\). Then \(C_{S(n)} \le 7\).

public theorem_wanted weightedConsecutiveConstant_squareSet_square_divisible_fiveFourth
    (n : ℕ) (hn : 2 ≤ n) (hnSquare : IsSquare n) (hdiv : 5 ^ 4 ∣ n) :
    weightedConsecutiveConstant n (squareSet n) ≤ 7

Sources

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

Uses 2

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

TheoremConsecutive square-weighted constant of the square of an odd squarefree number#●ready to prove

Let \(m\) be an odd squarefree natural number and let \(n = m^2\) with \(n \ge 2\). Write \(S(n)\) for the set of nonzero squares of \(\mathbb{Z}/n\mathbb{Z}\). Then there is a positive length \(k\) such that every sequence \(x_1, \dots, x_k\) in \(\mathbb{Z}/n\mathbb{Z}\) has a nonempty block of consecutive terms \(x_i, \dots, x_j\) and weights \(a_i, \dots, a_j \in S(n)\) with \(a_i x_i + \dots + a_j x_j = 0\), and the consecutive \(S(n)\)-weighted zero-sum constant \(C_{S(n)}\), the least such \(k\), equals \(9\).

The hypothesis \(n \ge 2\) is the paper's standing convention.

public theorem_wanted weightedConsecutiveConstant_squareSet_square_oddSquarefree
    (n m : ℕ) (hn : 2 ≤ n) (hnm : n = m ^ 2) (hmOdd : Odd m)
    (hmSquarefree : Squarefree m) :
    (weightedConsecutiveDefiningSet n (squareSet n)).Nonempty ∧
      weightedConsecutiveConstant n (squareSet n) = 9

Sources

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

Uses 3

Statement usesNonzero squares modulo \(n\) · Weighted consecutive zero-sum constant · Lengths forcing a consecutive weighted zero sum

TheoremXia's theorem on arithmetic progressions of weights#●ready to prove

Let \(n \ge 2\) and \(a\) be natural numbers, and let \(A = \{(a + i) \bmod n : 0 \le i < \lceil n/2 \rceil\}\) be the set of remainders modulo \(n\) of the \(\lceil n/2 \rceil\) consecutive integers \(a, a + 1, \dots, a + \lceil n/2 \rceil - 1\). If \(0 \notin A\), then the \(A\)-weighted Davenport constant of \(\mathbb{Z}/n\mathbb{Z}\) is \(D_A(\mathbb{Z}/n\mathbb{Z}) = 2\).

public theorem_wanted weightedDavenport_zmod_arithmeticProgression (n a : ℕ) (hn : 2 ≤ n)
    (hzero : 0 ∉ (Finset.range (n ⌈/⌉ 2)).image (fun i => (a + i) % n)) :
    weightedDavenport ((Finset.range (n ⌈/⌉ 2)).image (fun i => (a + i) % n)) (ZMod n) =
      ((2 : ℕ) : ℕ∞)

Sources

• Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Theorem 1.

Uses 1

Statement usesWeighted Davenport constant

TheoremWeighted Davenport constant of \(\mathbb{Z}/n\mathbb{Z}\) for the weights prime to \(p\)#●ready to prove

Let \(n\) be a positive integer, \(p\) a prime dividing \(n\) and \(k = v_p(n)\) the exponent of \(p\) in \(n\). For the weight set \(A = \{a \in \{1, \dots, n - 1\} : p \nmid a\}\), the \(A\)-weighted Davenport constant of \(\mathbb{Z}/n\mathbb{Z}\) is \(D_A(\mathbb{Z}/n\mathbb{Z}) = k + 1\).

This is Xia's theorem. Without the hypothesis \(p \mid n\) the formula fails: for \(n = 10\) and \(p = 3\) one has \(v_3(10) = 0\) but \(D_A(\mathbb{Z}/10\mathbb{Z}) = 2\).

public theorem_wanted weightedDavenport_zmod_not_dvd_prime (n p : ℕ) (hp : p.Prime)
    (hpn : p ∣ n) (hn : 0 < n) :
    weightedDavenport ((Finset.Icc 1 (n - 1)).filter (fun a => ¬ p ∣ a)) (ZMod n) =
      ((padicValNat p n + 1 : ℕ) : ℕ∞)

Sources

• Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Theorem 2.

Uses 1

Statement usesWeighted Davenport constant

TheoremOlson's theorem for groups of rank at most two#●ready to prove

For positive integers \(h\) and \(k\) with \(h \mid k\), the Davenport constant \(D(G) = D_{\{1\}}(G)\) of \(G = \mathbb{Z}/h\mathbb{Z} \oplus \mathbb{Z}/k\mathbb{Z}\) is \(D(G) = h + k - 1\).

public theorem_wanted weightedDavenport_one_zmod_prod_of_dvd (h k : ℕ) (hh : 1 ≤ h)
    (hdvd : h ∣ k) (hk : 1 ≤ k) :
    weightedDavenport {1} (ZMod h × ZMod k) = ((h + k - 1 : ℕ) : ℕ∞)

Sources

• Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Theorem 3.

Uses 1

Statement usesWeighted Davenport constant

TheoremOlson's theorem for abelian \(p\)-groups#●ready to prove

Let \(p\) be a prime, \(r \ge 0\) and let \(e_1, \dots, e_r \ge 1\) be natural numbers. The Davenport constant \(D(G) = D_{\{1\}}(G)\) of \(G = \mathbb{Z}/p^{e_1}\mathbb{Z} \oplus \dots \oplus \mathbb{Z}/p^{e_r}\mathbb{Z}\) is \(D(G) = 1 + \sum_{i=1}^{r} (p^{e_i} - 1)\). For \(r = 0\) the group \(G\) is trivial and this reads \(D(G) = 1\).

public theorem_wanted weightedDavenport_one_pi_zmod_prime_pow (p r : ℕ) (hp : p.Prime)
    (e : Fin r → ℕ) (he : ∀ i, 1 ≤ e i) :
    weightedDavenport {1} ((i : Fin r) → ZMod (p ^ e i)) =
      ((1 + ∑ i, (p ^ e i - 1) : ℕ) : ℕ∞)

Sources

• Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Theorem 4.

Uses 1

Statement usesWeighted Davenport constant

TheoremA nested ceiling identity for divisors#●ready to prove

For all natural numbers \(m, n \ge 2\) with \(m \mid n\), we have \(\lceil n / (\lceil n/(m-1) \rceil - 1) \rceil = m\).

public theorem_wanted ceilDiv_ceilDiv_sub_one_sub_one_of_dvd (m n : ℕ) (hm : 2 ≤ m)
    (hn : 2 ≤ n) (hdvd : m ∣ n) :
    n ⌈/⌉ (n ⌈/⌉ (m - 1) - 1) = m

Sources

• Md Ibrahim Molla, New Families of Weight Sets Yielding Prescribed Weighted Zero-Sum Constants, INTEGERS 26 (2026), Article A89, Lemma 1.

20 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.