Ducci sequences

DefinitionDucci coefficients#✓fully proved

For natural numbers \(n\), \(r\) and \(s\), the Ducci coefficient is \(a_{r,s} = \sum_{0 \le j \le r,\ j \equiv s - 1 \ (\mathrm{mod}\ n)} \binom{r}{j}\), where \(s - 1\) is read as \(0\) when \(s = 0\) and congruence modulo \(0\) is equality.

For \(1 \le s \le n\), \(a_{r,s}\) is the coefficient of \(x_s\) in the first entry of \(D^r(x)\), where the Ducci map \(D\) on \(\mathbb{Z}_m^n\) sends \((x_1, \dots, x_n)\) to \((x_1 + x_2, x_2 + x_3, \dots, x_n + x_1)\).

def ducciCoeff (n r s : ℕ) : ℕ :=
  ∑ j ∈ (Finset.range (r + 1)).filter
    (fun j => j % n = (s - 1) % n), Nat.choose r j
Used by 2
Used byReduction of Ducci coefficients modulo \(p\) · Vanishing of Ducci coefficients modulo \(p\)

TheoremBinomial coefficients \(\binom{p^k - 1}{j}\) modulo \(p\)#●ready to prove

Let \(p\) be a prime, let \(k \ge 1\), and let \(j\) be an integer with \(0 \le j \le p^k - 1\). Then \(\binom{p^k - 1}{j} \equiv (-1)^j \pmod{p}\).

theorem_wanted choose_prime_pow_sub_one_mod (p k j : ℕ)
    (hp : p.Prime) (hk : 1 ≤ k) (hj : j ≤ p ^ k - 1) :
    ((Nat.choose (p ^ k - 1) j : ℤ) : ZMod p) = (-1) ^ j
Sources
  • Mark L. Lewis and Shannon M. Tefft, "The Maximum Length for Ducci Sequences on ℤ_m^n when n is Even", Lemma 1.

TheoremBinomial coefficients \(\binom{p^k - p^{k-1}}{j}\) modulo \(p\)#●ready to prove

Let \(p\) be an odd prime, let \(k \ge 2\), and let \(j\) be an integer with \(0 \le j \le p^k - p^{k-1}\). If \(j = c\,p^{k-1}\) for an integer \(c\), then \(\binom{p^k - p^{k-1}}{j} \equiv (-1)^c \pmod{p}\); otherwise \(\binom{p^k - p^{k-1}}{j} \equiv 0 \pmod{p}\).

theorem_wanted choose_prime_pow_sub_mod (p k j : ℕ)
    (hp : p.Prime) (hpo : p ≠ 2) (hk : 2 ≤ k)
    (hj : j ≤ p ^ k - p ^ (k - 1)) :
    ((Nat.choose (p ^ k - p ^ (k - 1)) j : ℤ) : ZMod p) =
      if j % p ^ (k - 1) = 0 then (-1) ^ (j / p ^ (k - 1))
      else 0
Sources
  • Mark L. Lewis and Shannon M. Tefft, "The Maximum Length for Ducci Sequences on ℤ_m^n when n is Even", Lemma 2.

TheoremVanishing of Ducci coefficients modulo \(p\)#●ready to prove

For integers \(N \ge 1\), \(r \ge 0\) and \(s \ge 1\) write \(a^{(N)}_{r,s} = \sum_{0 \le j \le r,\ j \equiv s - 1 \ (\mathrm{mod}\ N)} \binom{r}{j}\) for the Ducci coefficients of length \(N\). Let \(p\) be a prime, let \(k \ge 0\) and \(n_1 \ge 2\) be integers, and let \(n = p^k n_1\). Let \(c \ge 1\), and let \(s\) be an integer with \(1 \le s \le n\) that is not of the form \(b\,p^k + 1\) with \(0 \le b < n_1\). Then \(a^{(n)}_{c p^k, s} \equiv 0 \pmod{p}\).

theorem_wanted ducciCoeff_vanish_mod (p k n1 c s : ℕ)
    (hp : p.Prime) (hn1 : 2 ≤ n1) (hc : 1 ≤ c)
    (hs1 : 1 ≤ s) (hs2 : s ≤ p ^ k * n1)
    (hs : ¬ ∃ b : ℕ, b < n1 ∧ s = b * p ^ k + 1) :
    ((ducciCoeff (p ^ k * n1) (c * p ^ k) s : ℤ) : ZMod p) = 0
Sources
  • Mark L. Lewis and Shannon M. Tefft, "The Maximum Length for Ducci Sequences on ℤ_m^n when n is Even", Lemma 3.
Uses 1
Statement usesDucci coefficients

TheoremReduction of Ducci coefficients modulo \(p\)#●ready to prove

For integers \(N \ge 1\), \(r \ge 0\) and \(s \ge 1\) write \(a^{(N)}_{r,s} = \sum_{0 \le j \le r,\ j \equiv s - 1 \ (\mathrm{mod}\ N)} \binom{r}{j}\) for the Ducci coefficients of length \(N\). Let \(p\) be a prime, let \(k \ge 0\) and \(n_1 \ge 2\) be integers, and let \(n = p^k n_1\). Then for every integer \(c \ge 1\) and every integer \(b\) with \(0 \le b < n_1\), \(a^{(n)}_{c p^k,\, b p^k + 1} \equiv a^{(n_1)}_{c,\, b + 1} \pmod{p}\).

theorem_wanted ducciCoeff_reduce_mod (p k n1 c b : ℕ)
    (hp : p.Prime) (hn1 : 2 ≤ n1) (hc : 1 ≤ c) (hb : b < n1) :
    ((ducciCoeff (p ^ k * n1) (c * p ^ k) (b * p ^ k + 1) : ℤ) :
      ZMod p) =
      ((ducciCoeff n1 c (b + 1) : ℤ) : ZMod p)
Sources
  • Mark L. Lewis and Shannon M. Tefft, "The Maximum Length for Ducci Sequences on ℤ_m^n when n is Even", Lemma 4.
Uses 1
Statement usesDucci coefficients

TheoremDucci predecessor criterion for even length#●ready to prove

Let \(m \ge 0\) be an integer, let \(n \ge 2\) be even, and write \(\mathbb{Z}_m = \mathbb{Z}/m\mathbb{Z}\) (so \(\mathbb{Z}_0 = \mathbb{Z}\)). A tuple \(x = (x_1, \dots, x_n) \in \mathbb{Z}_m^n\) has a Ducci predecessor, that is, a tuple \(y \in \mathbb{Z}_m^n\) with \(y_i + y_{i+1} = x_i\) for all \(i\) (indices taken cyclically, so \(y_{n+1} = y_1\)), if and only if \(x_1 - x_2 + x_3 - \cdots + x_{n-1} - x_n = 0\) in \(\mathbb{Z}_m\).

theorem_wanted ducci_pred_iff (m n : ℕ) [NeZero n]
    (hn : Even n) (x : Fin n → ZMod m) :
    (∃ y : Fin n → ZMod m, ∀ i : Fin n, y i + y (i + 1) = x i) ↔
      ∑ i : Fin n, (-1 : ZMod m) ^ i.val * x i = 0
Sources
  • Mark L. Lewis and Shannon M. Tefft, "The Maximum Length for Ducci Sequences on ℤ_m^n when n is Even", Theorem 2.
1 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.