Permutation polynomials

DefinitionPermutation polynomial over a finite field#✓fully proved

A polynomial \(f\) over a finite field \(F\) is a permutation polynomial when its evaluation map \(F \to F\), \(x \mapsto f(x)\), is bijective.

def IsPermutationPolynomial {F : Type*} [Field F] [Finite F]
    (f : Polynomial F) : Prop :=
  Function.Bijective fun x => f.eval x
Used by 8

DefinitionPolynomial complete to level \(k\)#✓fully proved

Let \(F\) be a finite field, \(f \in F[X]\) and \(k\) a natural number. The polynomial \(f\) is complete to level \(k\) (\(k\)-complete) when \(f + iX\) is a permutation polynomial for every natural number \(i \le k\), where \(i\) is viewed as an element of \(F\).

The source considers only positive levels \(k\); here every natural level is allowed, and completeness to level \(0\) says that \(f\) itself is a permutation polynomial.

def IsKComplete {F : Type*} [Field F] [Finite F] (f : Polynomial F)
    (k : ℕ) : Prop :=
  ∀ i : ℕ, i ≤ k → IsPermutationPolynomial (f + Polynomial.C (i : F) * Polynomial.X)
Uses 1 · Used by 5

TheoremUnfolded form of \(k\)-completeness#✓fully proved

Let \(F\) be a finite field, \(f \in F[X]\) and \(k\) a natural number. Then \(f\) is complete to level \(k\) if and only if for every natural number \(i \le k\) the map \(F \to F\), \(x \mapsto (f + iX)(x)\), is bijective, where \(i\) is viewed as an element of \(F\).

theorem isKComplete_iff {F : Type*} [Field F] [Finite F] (f : Polynomial F)
    (k : ℕ) :
    IsKComplete f k ↔ ∀ i : ℕ, i ≤ k →
      Function.Bijective fun x =>
        (f + Polynomial.C (i : F) * Polynomial.X).eval x
Uses 1

TheoremCompleteness at a lower level#✓fully proved

Let \(F\) be a finite field, \(f \in F[X]\) and let \(j \le k\) be natural numbers. If \(f\) is complete to level \(k\), then \(f\) is complete to level \(j\).

theorem isKComplete_mono {F : Type*} [Field F] [Finite F] {f : Polynomial F}
    {j k : ℕ} (h : IsKComplete f k) (hle : j ≤ k) : IsKComplete f j
Uses 1

TheoremCompleteness at level zero#✓fully proved

Let \(F\) be a finite field and \(f \in F[X]\). Then \(f\) is complete to level \(0\) if and only if \(f\) is a permutation polynomial.

theorem isKComplete_zero {F : Type*} [Field F] [Finite F] (f : Polynomial F) :
    IsKComplete f 0 ↔ IsPermutationPolynomial f
Uses 2

TheoremCompleteness at the next level#✓fully proved

Let \(F\) be a finite field, \(f \in F[X]\) and \(k\) a natural number. Then \(f\) is complete to level \(k + 1\) if and only if \(f\) is complete to level \(k\) and \(f + (k + 1)X\) is a permutation polynomial, where \(k + 1\) is viewed as an element of \(F\).

theorem isKComplete_succ_iff {F : Type*} [Field F] [Finite F]
    (f : Polynomial F) (k : ℕ) :
    IsKComplete f (k + 1) ↔ IsKComplete f k ∧
      IsPermutationPolynomial
        (f + Polynomial.C ((k + 1 : ℕ) : F) * Polynomial.X)
Uses 2

TheoremA \(k\)-complete polynomial is a permutation polynomial#✓fully proved

Let \(F\) be a finite field, \(f \in F[X]\) and \(k\) a natural number. If \(f\) is complete to level \(k\), then \(f\) is a permutation polynomial.

theorem isKComplete_self {F : Type*} [Field F] [Finite F] {f : Polynomial F}
    {k : ℕ} (h : IsKComplete f k) : IsPermutationPolynomial f
Uses 2

TheoremHermite–Dickson criterion#✓fully proved

Let \(\mathbb{F}_q\) be a finite field with \(q\) elements and characteristic \(p\), and let \(f \in \mathbb{F}_q[X]\). Then \(f\) is a permutation polynomial of \(\mathbb{F}_q\), that is, \(x \mapsto f(x)\) is a bijection of \(\mathbb{F}_q\), if and only if \(f\) has exactly one root in \(\mathbb{F}_q\) and, for every integer \(t\) with \(1 \le t \le q - 2\) and \(p \nmid t\), the remainder of \(f^t\) upon division by \(X^q - X\) has degree at most \(q - 2\).

theorem hermite_dickson_permutation_criterion
    {p : ℕ} {Fq : Type*} [Field Fq] [Fintype Fq] [DecidableEq Fq] [CharP Fq p]
    [Fact p.Prime] (hq : 2 ≤ Fintype.card Fq) (f : Polynomial Fq) :
    let q := Fintype.card Fq
    Polynomial.IsPermutationPolynomial f ↔
      (Finset.univ.filter (fun x => Polynomial.eval x f = 0)).card = 1 ∧
        ∀ t : ℕ, 1 ≤ t → t ≤ q - 2 → ¬ p ∣ t →
          Polynomial.natDegree ((f ^ t) % (Polynomial.X ^ q - Polynomial.X)) ≤ q - 2
Sources
  • Brian G. Kronenthal, "An Integer Sequence Motivated by Generalized Quadrangles", Journal of Integer Sequences 18 (2015), Article 15.7.8, https://cs.uwaterloo.ca/journals/JIS/VOL18/Kronenthal/kron3.tex, Hermite–Dickson statement at lines 120–126.
Uses 1

TheoremMonomial permutation polynomials of a finite field#●ready to prove

Let \(K\) be a finite field with \(q\) elements and let \(d \ge 1\) be an integer. Then \(X^d\) is a permutation polynomial of \(K\) if and only if \(\gcd(d, q - 1) = 1\).

The hypothesis \(d \ge 1\) is needed: for \(d = 0\) and \(q = 2\) the condition \(\gcd(d, q - 1) = 1\) holds, but \(X^0 = 1\) is constant.

public theorem_wanted isPermutationPolynomial_X_pow_iff_coprime {K : Type*} [Field K]
    [Fintype K] {d : ℕ} (hd : 0 < d) :
    (X ^ d : K[X]).IsPermutationPolynomial ↔ d.Coprime (Fintype.card K - 1)
Sources
  • Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Lemma 2.
Uses 1

TheoremPower-sum criterion for distinct elements of a finite field#●ready to prove

Let \(K\) be a finite field with \(q\) elements and let \(a_1, \dots, a_q \in K\). Then \(a_1, \dots, a_q\) are pairwise distinct if and only if \(\sum_{i=1}^{q} a_i^t = 0\) for every \(t = 0, 1, \dots, q - 2\) and \(\sum_{i=1}^{q} a_i^{q-1} = -1\), where \(0^0 = 1\).

public theorem_wanted injective_iff_sum_pow_eq {K : Type*} [Field K] [Fintype K]
    (a : Fin (Fintype.card K) → K) :
    Function.Injective a ↔
      (∀ t : ℕ, t < Fintype.card K - 1 → ∑ i, a i ^ t = 0) ∧
        ∑ i, a i ^ (Fintype.card K - 1) = -1
Sources
  • Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Lemma 3.

TheoremAlternating binomial sums of powers#●ready to prove

Let \(x, y, k \in \mathbb{C}\) and let \(n, m\) be positive integers. If \(n = m\), then

\[\sum_{i=0}^{n} (-1)^i \binom{n}{i} (kx + iy)^m = (-1)^n y^n n!,\]

and if \(m < n\), then \(\sum_{i=0}^{n} (-1)^i \binom{n}{i} (kx + iy)^m = 0\).

public theorem_wanted sum_neg_one_pow_choose_mul_pow (x y k : ℂ) {n m : ℕ} (hn : 0 < n)
    (hm : 0 < m) :
    (n = m → ∑ i ∈ Finset.range (n + 1),
        (-1 : ℂ) ^ i * (n.choose i : ℂ) * (k * x + i * y) ^ m =
          (-1) ^ n * y ^ n * (n.factorial : ℂ)) ∧
      (m < n → ∑ i ∈ Finset.range (n + 1),
        (-1 : ℂ) ^ i * (n.choose i : ℂ) * (k * x + i * y) ^ m = 0)
Sources
  • Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Theorem 3.

TheoremShifted power-sum permutation polynomials of a prime field#●ready to prove

Let \(p\) be an odd prime and let \(k, t, a\) be positive integers with \(\gcd(a + 1, p - 1) = 1\) and \(k \equiv 1 \pmod{p(p-1)}\). Suppose that \(p - 1 \nmid t\) or \(p^2 \mid k - 1\). Then the polynomial \(\sum_{n=1}^{k} n^t X^{n+a}\), with coefficients reduced modulo \(p\), is a permutation polynomial of \(\mathbb{F}_p\).

public theorem_wanted isPermutationPolynomial_sum_pow_mul_X_pow_add {p : ℕ} [Fact p.Prime]
    (hp : p ≠ 2) {k t a : ℕ} (hk : 0 < k) (ht : 0 < t) (ha : 0 < a)
    (hka : (a + 1).Coprime (p - 1)) (hkcong : k ≡ 1 [MOD p * (p - 1)])
    (hcases : ¬(p - 1) ∣ t ∨ p ^ 2 ∣ k - 1) :
    (∑ n ∈ Finset.Icc 1 k, C ((n : ZMod p) ^ t) * X ^ (n + a)).IsPermutationPolynomial
Sources
  • Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Corollary 1.
Uses 1

TheoremDilated power-sum permutation polynomials of a prime field#●ready to prove

Let \(p\) be an odd prime and let \(k, t, a\) be positive integers with \(p \nmid a\), \(\gcd(a, p - 1) = 1\) and \(k \equiv 1 \pmod{p(p-1)}\). Suppose that \(p - 1 \nmid t\) or \(p^2 \mid k - 1\). Then the polynomial \(\sum_{n=1}^{k} (an)^t X^{an}\), with coefficients reduced modulo \(p\), is a permutation polynomial of \(\mathbb{F}_p\).

public theorem_wanted isPermutationPolynomial_sum_mul_pow_mul_X_pow_mul {p : ℕ}
    [Fact p.Prime] (hp : p ≠ 2) {k t a : ℕ} (hk : 0 < k) (ht : 0 < t) (ha : 0 < a)
    (hpa : ¬p ∣ a) (hap : a.Coprime (p - 1)) (hkcong : k ≡ 1 [MOD p * (p - 1)])
    (hcases : ¬(p - 1) ∣ t ∨ p ^ 2 ∣ k - 1) :
    (∑ n ∈ Finset.Icc 1 k,
      C (((a * n : ℕ) : ZMod p) ^ t) * X ^ (a * n)).IsPermutationPolynomial
Sources
  • Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Corollary 3.
Uses 1

TheoremRational form of the power-weighted geometric sum#●ready to prove

For positive integers \(t\) and \(k\), the following identity holds in \(\mathbb{Z}[X]\):

\[(1 - X)^{t+1} \sum_{n=1}^{k} n^t X^n = \sum_{n=1}^{t} \Bigl(\sum_{i=0}^{n-1} (-1)^i \binom{t+1}{i} (n - i)^t\Bigr) X^n + \sum_{m=1}^{t+1} \Bigl(\sum_{i=m}^{t+1} (-1)^i \binom{t+1}{i} (k + m - i)^t\Bigr) X^{k+m}.\]

Equivalently, for every \(x \ne 1\) the value \(h_t^k(x) = \sum_{n=1}^{k} n^t x^n\) is the right-hand side at \(x\) divided by \((1 - x)^{t+1}\), which is the form the source states.

public theorem_wanted one_sub_X_pow_mul_sum_pow_mul_X_pow (t k : ℕ) (ht : 0 < t) (hk : 0 < k) :
    (1 - X : ℤ[X]) ^ (t + 1) * ∑ n ∈ Finset.Icc 1 k, C ((n : ℤ) ^ t) * X ^ n =
      ∑ n ∈ Finset.Icc 1 t, C (∑ i ∈ Finset.range n,
          (-1) ^ i * ((t + 1).choose i : ℤ) * ((n : ℤ) - i) ^ t) * X ^ n +
        ∑ m ∈ Finset.Icc 1 (t + 1), C (∑ i ∈ Finset.Icc m (t + 1),
          (-1) ^ i * ((t + 1).choose i : ℤ) * ((k : ℤ) + m - i) ^ t) * X ^ (k + m)
Sources
  • Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Lemma 4.

TheoremVishwakarma–Singh congruence for ordered partitions#●ready to prove

Let \(p\) be an odd prime and let \(k, s, t\) be positive integers with \(s \le p - 2\) and \(k \equiv 1 \pmod{p(p-1)}\), such that \(p^2 \mid k - 1\) whenever \(p - 1 \mid t\). Let \(\mu = \lfloor ks/(p - 1) \rfloor\). Then

\[\sum_{j=1}^{\mu} \sum_{\omega} (\omega_1 \cdots \omega_s)^t \equiv 0 \pmod{p},\]

where for each \(j\) the inner sum runs over all \(s\)-tuples \(\omega = (\omega_1, \dots, \omega_s)\) with entries in \(\{1, \dots, k\}\) and \(\omega_1 + \cdots + \omega_s = j(p - 1)\).

The source states the hypothesis \(s \not\equiv 0 \pmod{p}\) in place of \(s \le p - 2\), the range of Hermite's criterion used in its proof; with that hypothesis the claim fails, e.g. for \(p = 3\), \(k = 1\), \(s = 2\), \(t = 1\) the sum is \(1\).

public theorem_wanted prime_dvd_sum_compositions_prod_pow {p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2)
    {k s t : ℕ} (hk : 0 < k) (hs : 0 < s) (hsp : s ≤ p - 2) (ht : 0 < t)
    (hkcong : k ≡ 1 [MOD p * (p - 1)]) (hcases : (p - 1) ∣ t → p ^ 2 ∣ k - 1) :
    p ∣ ∑ j ∈ Finset.Icc 1 (k * s / (p - 1)),
      ∑ ω ∈ (Fintype.piFinset fun _ : Fin s => Finset.Icc 1 k).filter
          (fun ω => ∑ i, ω i = j * (p - 1)),
        (∏ i, ω i) ^ t
Sources
  • Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Theorem 1.

TheoremVishwakarma–Singh congruence for ordered partitions, linear case#●ready to prove

Let \(p\) be an odd prime and let \(k, s\) be positive integers with \(s \le p - 2\) and \(k \equiv 1 \pmod{p(p-1)}\). Let \(\mu = \lfloor ks/(p - 1) \rfloor\). Then

\[\sum_{j=1}^{\mu} \sum_{\omega} \omega_1 \cdots \omega_s \equiv 0 \pmod{p},\]

where for each \(j\) the inner sum runs over all \(s\)-tuples \(\omega = (\omega_1, \dots, \omega_s)\) with entries in \(\{1, \dots, k\}\) and \(\omega_1 + \cdots + \omega_s = j(p - 1)\).

This is the case \(t = 1\) of the source's Theorem 1. The source states the hypothesis \(s \not\equiv 0 \pmod{p}\) in place of \(s \le p - 2\); with that hypothesis the claim fails, e.g. for \(p = 3\), \(k = 7\), \(s = 2\) the sum is \(400 \equiv 1 \pmod{3}\).

public theorem_wanted prime_dvd_sum_compositions_prod {p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2)
    {k s : ℕ} (hk : 0 < k) (hs : 0 < s) (hsp : s ≤ p - 2) (hkcong : k ≡ 1 [MOD p * (p - 1)]) :
    p ∣ ∑ j ∈ Finset.Icc 1 (k * s / (p - 1)),
      ∑ ω ∈ (Fintype.piFinset fun _ : Fin s => Finset.Icc 1 k).filter
          (fun ω => ∑ i, ω i = j * (p - 1)),
        ∏ i, ω i
Sources
  • Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Corollary 2.

TheoremVishwakarma–Singh congruence for ordered partitions into multiples#●ready to prove

Let \(p\) be an odd prime and let \(a, k, s, t\) be positive integers with \(\gcd(a, p - 1) = 1\), \(s \le p - 2\) and \(k \equiv 1 \pmod{p(p-1)}\), such that \(p^2 \mid k - 1\) whenever \(p - 1 \mid t\). Let \(\mu = \lfloor aks/(p - 1) \rfloor\). Then

\[\sum_{j=1}^{\mu} \sum_{\omega} (\omega_1 \cdots \omega_s)^t \equiv 0 \pmod{p},\]

where for each \(j\) the inner sum runs over all \(s\)-tuples \(\omega = (\omega_1, \dots, \omega_s)\) with entries in \(\{an : 1 \le n \le k\}\) and \(\omega_1 + \cdots + \omega_s = j(p - 1)\).

The source states this with two differences. It assumes \(s \not\equiv 0 \pmod{p}\) in place of \(s \le p - 2\); with that hypothesis the claim fails, e.g. for \(a = 1\), \(p = 3\), \(k = 7\), \(s = 2\), \(t = 1\). It takes \(\mu = \lfloor ks/(p - 1) \rfloor\); with that bound the claim fails for \(a > 1\), e.g. for \(p = 5\), \(a = 3\), \(k = 21\), \(s = t = 1\) the sum is \(12\). The bound \(\lfloor aks/(p - 1) \rfloor\) covers every multiple of \(p - 1\) up to \(aks\), the degree of the \(s\)-th power of \(\sum_{n=1}^{k} (an)^t X^{an}\), to which the proof applies Hermite's criterion.

public theorem_wanted prime_dvd_sum_compositions_mul_prod_pow {p : ℕ} (hp : p.Prime)
    (hp2 : p ≠ 2) {a k s t : ℕ} (ha : 0 < a) (hap : a.Coprime (p - 1)) (hk : 0 < k) (hs : 0 < s)
    (hsp : s ≤ p - 2) (ht : 0 < t) (hkcong : k ≡ 1 [MOD p * (p - 1)])
    (hcases : (p - 1) ∣ t → p ^ 2 ∣ k - 1) :
    p ∣ ∑ j ∈ Finset.Icc 1 (a * k * s / (p - 1)),
      ∑ ω ∈ (Fintype.piFinset fun _ : Fin s => (Finset.Icc 1 k).image (a * ·)).filter
          (fun ω => ∑ i, ω i = j * (p - 1)),
        (∏ i, ω i) ^ t
Sources
  • Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Corollary 4.

TheoremPower sums over \(\mathbb{Z}/p\mathbb{Z}\)#●ready to prove

Let \(p\) be a prime and \(t\) a positive integer. Then \(\sum_{a \in \mathbb{Z}/p\mathbb{Z}} a^t\) equals \(-1\) if \(p - 1\) divides \(t\), and \(0\) otherwise.

theorem_wanted sum_zmod_pow_eq_ite
    (p t : ℕ) [NeZero p] (hp : p.Prime) (ht : 0 < t) :
    (∑ a : ZMod p, a ^ t) = if (p - 1) ∣ t then -1 else 0
Sources
  • Zhiguo Ding and Michael E. Zieve, "Permutation Polynomials of the Form ∑_{n=1}^k h(n) X^n", Lemma 1.

TheoremPermutation polynomials \(\sum_{n=1}^k n^t X^n\) over \(\mathbb{F}_p\)#●ready to prove

Let \(p\) be an odd prime and let \(k\) and \(t\) be positive integers with \(k \equiv 1 \pmod{p(p-1)}\). Suppose that \(k \equiv 1 \pmod{p^2}\) or that \(p - 1\) does not divide \(t\). Then the map \(c \mapsto \sum_{n=1}^{k} n^t c^n\) is a bijection from \(\mathbb{Z}/p\mathbb{Z}\) to itself.

Ding and Zieve quote this result from an earlier paper.

theorem_wanted bijective_sum_pow_mul_pow_zmod
    (p k t : ℕ) (hp : p.Prime) (hpodd : p % 2 = 1)
    (hk : 0 < k) (ht : 0 < t)
    (hkcong : k % (p * (p - 1)) = 1)
    (hcases : k % (p ^ 2) = 1 ∨ ¬(p - 1) ∣ t) :
    Function.Bijective
      (fun c : ZMod p =>
        ∑ n ∈ Finset.Icc 1 k, (n : ZMod p) ^ t * c ^ n)
Sources
  • Zhiguo Ding and Michael E. Zieve, "Permutation Polynomials of the Form ∑_{n=1}^k h(n) X^n", Theorem 1.

TheoremWhen \(\sum_{n=1}^k h(n) X^n\) induces the identity on \(\mathbb{F}_q\)#●ready to prove

Let \(p\) be a prime, \(\ell \ge 1\) and \(q = p^\ell > 2\), and let \(K\) be a finite field of characteristic \(p\) with \(q\) elements. Let \(k\) be a positive integer with \(k \equiv 1 \pmod{p(q-1)}\) and let \(h \in K[X]\), with degree \(d\) (taken to be \(0\) when \(h = 0\)) and coefficient \(h_i\) of \(X^i\). Then \(\sum_{n=1}^{k} h(n)\,c^n = c\) for every \(c \in K\) if and only if \(h(1) = 1\) and either \(k \equiv 1 \pmod{p^2}\) or \(\sum_{j=1}^{\lfloor d/(p-1) \rfloor} h_{j(p-1)} = 0\).

theorem_wanted finiteField_sum_eval_mul_pow_eq_id_iff
    (K : Type*) [Field K] [Fintype K] (p ℓ : ℕ) [CharP K p]
    (hp : p.Prime) (hℓ : 0 < ℓ)
    (hcard : Fintype.card K = p ^ ℓ) (hq : 2 < p ^ ℓ)
    (k : ℕ) (hk : 0 < k)
    (hkcong : k % (p * (p ^ ℓ - 1)) = 1)
    (h : Polynomial K) :
    (∀ c : K, (∑ n ∈ Finset.Icc 1 k, h.eval (n : K) * c ^ n) = c) ↔
      h.eval 1 = 1 ∧
        (k % (p ^ 2) = 1 ∨
          (∑ j ∈ Finset.Icc 1 (h.natDegree / (p - 1)),
            h.coeff (j * (p - 1))) = 0)
Sources
  • Zhiguo Ding and Michael E. Zieve, "Permutation Polynomials of the Form ∑_{n=1}^k h(n) X^n", Theorem 2.
8 fully proved12 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.