Linearized and subspace polynomials over fields of characteristic two

A polynomial over a field of characteristic two is linearized when every exponent occurring in it is a power of two. Such a polynomial evaluates to an additive, hence 𝔽₂-linear, function. The subspace polynomial ∏_{c ∈ 𝔽₂ᵐ} (X - ∑ cₗ bₗ) of a family b is linearized, monic of degree 2 ^ m, and its roots are the 𝔽₂-span of b [Ore33].

Over a finite field F with 2 ^ n elements every 𝔽₂-subspace W of dimension d is the image of a monic linearized polynomial of degree 2 ^ (n - d), its image-subspace polynomial [BenSassonKopparty2012, Lemma 3.7]. Writing that polynomial as ∑_{j ∈ ℤ/n} a j X ^ 2 ^ j, the coefficients vanish at the d - 1 positions above the leading one; the structural lemma [BenSassonKopparty2012, Lemma 3.10] says that, apart from this canonical run, no d - 1 consecutive coefficients vanish unless W lies in a multiple of a proper subfield. We record it for subspaces of dimension larger than every proper subfield, which is how it is used for composite-degree fields.

Main definitions

• Cslib.IsLinearized: every exponent of a polynomial is a power of two.
• Cslib.IsLinearized.toLinearMap: the 𝔽₂-linear map given by evaluating a linearized polynomial.
• Cslib.subspacePoly: the subspace polynomial of a finite family.
• Cslib.linearizedEval: evaluation of a coefficient vector indexed by ZMod n.
• Cslib.CoeffPattern: the zero pattern of an image-subspace polynomial.

Main results

• Cslib.isLinearized_subspacePoly, Cslib.eval_subspacePoly_eq_zero_iff: subspace polynomials are linearized and vanish exactly on the span.
• Cslib.exists_isLinearized_range_eq: the image-subspace polynomial.
• Cslib.eq_zero_of_linearizedEval_eq_zero: a nonzero linearized function of 2-degree below m has fewer than 2 ^ m roots.
• Cslib.exists_coeffPattern: the structural lemma, for subspaces of dimension larger than every proper subfield.

References

• O. Ore, On a special class of polynomials
• E. Ben-Sasson, S. Kopparty, Affine dispersers from subspace polynomials

Linearized polynomials

def Cslib.IsLinearized {F : Type u_1} [Field F] (P : Polynomial F) : Prop

A polynomial is linearized (over 𝔽₂) when every exponent with a nonzero coefficient is a power of two. Over a field of characteristic two it evaluates to an additive function.

theorem Cslib.IsLinearized.zero {F : Type u_1} [Field F] : IsLinearized 0

The zero polynomial is linearized.

theorem Cslib.IsLinearized.add {F : Type u_1} [Field F] {P Q : Polynomial F} (hP : IsLinearized P) (hQ : IsLinearized Q) : IsLinearized (P + Q)

A sum of linearized polynomials is linearized.

theorem Cslib.IsLinearized.C_mul {F : Type u_1} [Field F] {P : Polynomial F} (hP : IsLinearized P) (c : F) : IsLinearized (Polynomial.C c * P)

A constant multiple C c * P of a linearized polynomial is linearized.

theorem Cslib.IsLinearized.X_pow_two_pow {F : Type u_1} [Field F] (j : ℕ) : IsLinearized (Polynomial.X ^ 2 ^ j)

The monomial X ^ 2 ^ j is linearized.

theorem Cslib.IsLinearized.sq {F : Type u_1} [Field F] {P : Polynomial F} [CharP F 2] (hP : IsLinearized P) : IsLinearized (P ^ 2)

In characteristic two, the square of a linearized polynomial is linearized.

theorem Cslib.IsLinearized.coeff_zero {F : Type u_1} [Field F] {P : Polynomial F} (hP : IsLinearized P) : P.coeff 0 = 0

A linearized polynomial has constant coefficient 0.

theorem Cslib.IsLinearized.comp_add {F : Type u_1} [Field F] {P : Polynomial F} [CharP F 2] (hP : IsLinearized P) (f g : Polynomial F) : P.comp (f + g) = P.comp f + P.comp g

A linearized polynomial composes additively.

theorem Cslib.IsLinearized.comp_sub {F : Type u_1} [Field F] {P : Polynomial F} [CharP F 2] (hP : IsLinearized P) (f g : Polynomial F) : P.comp (f - g) = P.comp f - P.comp g

In characteristic two, a linearized polynomial composes subtractively: P.comp (f - g) = P.comp f - P.comp g.

theorem Cslib.IsLinearized.eval_add {F : Type u_1} [Field F] {P : Polynomial F} [CharP F 2] (hP : IsLinearized P) (x y : F) : Polynomial.eval (x + y) P = Polynomial.eval x P + Polynomial.eval y P

In characteristic two, a linearized polynomial evaluates additively: P.eval (x + y) = P.eval x + P.eval y.

theorem Cslib.IsLinearized.eval_zero {F : Type u_1} [Field F] {P : Polynomial F} (hP : IsLinearized P) : Polynomial.eval 0 P = 0

A linearized polynomial vanishes at 0.

def Cslib.IsLinearized.toLinearMap {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {P : Polynomial F} (hP : IsLinearized P) : F →ₗ[ZMod 2] F

The 𝔽₂-linear map given by evaluating a linearized polynomial.

@[simp]

theorem Cslib.IsLinearized.toLinearMap_apply {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {P : Polynomial F} (hP : IsLinearized P) (x : F) : hP.toLinearMap x = Polynomial.eval x P

The linear map of a linearized polynomial P sends x to P.eval x.

Subspace polynomials

noncomputable def Cslib.subspacePoly {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m : ℕ} (b : Fin m → F) : Polynomial F

The subspace polynomial ∏_{c ∈ 𝔽₂ᵐ} (X - ∑ₗ cₗ bₗ) of a family b of m elements.

theorem Cslib.monic_subspacePoly {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m : ℕ} (b : Fin m → F) : (subspacePoly b).Monic

The subspace polynomial is monic.

theorem Cslib.natDegree_subspacePoly {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m : ℕ} (b : Fin m → F) : (subspacePoly b).natDegree = 2 ^ m

The subspace polynomial of a family of m elements has degree 2 ^ m.

theorem Cslib.subspacePoly_snoc {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m : ℕ} (b : Fin m → F) (v : F) : subspacePoly (Fin.snoc b v) = subspacePoly b * (subspacePoly b).comp (Polynomial.X - Polynomial.C v)

The subspace polynomial of Fin.snoc b v is P * P.comp (X - C v) for P the subspace polynomial of b.

theorem Cslib.isLinearized_subspacePoly {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m : ℕ} (b : Fin m → F) : IsLinearized (subspacePoly b)

Subspace polynomials are linearized [Ore33].

theorem Cslib.eval_subspacePoly_eq_zero_iff {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m : ℕ} (b : Fin m → F) (x : F) : Polynomial.eval x (subspacePoly b) = 0 ↔ x ∈ Submodule.span (ZMod 2) (Set.range b)

The roots of the subspace polynomial of b are the 𝔽₂-span of b.

theorem Cslib.exists_isLinearized_range_eq {F : Type u_1} [Field F] [Algebra (ZMod 2) F] [Finite F] (W : Submodule (ZMod 2) F) : ∃ (Q : Polynomial F), IsLinearized Q ∧ Q.Monic ∧ Q.natDegree = 2 ^ (Module.finrank (ZMod 2) F - Module.finrank (ZMod 2) ↥W) ∧ ∀ (y : F), y ∈ W ↔ ∃ (x : F), Polynomial.eval x Q = y

Image-subspace polynomial [BenSassonKopparty2012, Lemma 3.7]: every 𝔽₂-subspace W of a finite field F is the image of a monic linearized polynomial of degree 2 ^ (dim F - dim W).

Coefficient vectors indexed by ZMod n

def Cslib.linearizedEval {F : Type u_1} [Field F] {n : ℕ} [NeZero n] (a : ZMod n → F) (x : F) : F

Evaluation of the linearized function x ↦ ∑_{j ∈ ℤ/n} a j * x ^ 2 ^ j. Over a field with 2 ^ n elements every linearized polynomial function has this form.

theorem Cslib.pow_two_pow_mod {F : Type u_1} [Field F] [Algebra (ZMod 2) F] [Finite F] {n : ℕ} (hn : Module.finrank (ZMod 2) F = n) (x : F) (m : ℕ) : x ^ 2 ^ m = x ^ 2 ^ (m % n)

Frobenius periodicity: in a field with 2 ^ n elements, x ^ 2 ^ m depends only on m % n.

theorem Cslib.linearizedEval_pow_two_pow {F : Type u_1} [Field F] [Algebra (ZMod 2) F] [Finite F] {n : ℕ} [NeZero n] (hn : Module.finrank (ZMod 2) F = n) (a : ZMod n → F) (k : ℕ) (x : F) : linearizedEval a x ^ 2 ^ k = linearizedEval (fun (j : ZMod n) => a (j - ↑k) ^ 2 ^ k) x

Raising a linearized function to the power 2 ^ k rotates its coefficient vector.

theorem Cslib.eq_zero_of_linearizedEval_eq_zero {F : Type u_1} [Field F] {n : ℕ} [NeZero n] {b : ZMod n → F} {m : ℕ} (hb : ∀ (j : ZMod n), m ≤ j.val → b j = 0) (S : Finset F) (hS : 2 ^ m ≤ S.card) (h : ∀ x ∈ S, linearizedEval b x = 0) : b = 0

Root bound for linearized functions: if the coefficients of b vanish from position m on and the function vanishes on at least 2 ^ m points, then b = 0.

theorem Cslib.exists_subfield_card_le {F : Type u_1} [Field F] [Algebra (ZMod 2) F] [Finite F] {n k : ℕ} (hn : Module.finrank (ZMod 2) F = n) (hk0 : 0 < k) (hkn : k < n) (W : Submodule (ZMod 2) F) (c : F) (h : ∀ y ∈ W, y ^ 2 ^ k = c * y) : ∃ (K : Subfield F), K ≠ ⊤ ∧ Nat.card ↥W ≤ Nat.card ↥K

If every element y of a subspace W satisfies y ^ 2 ^ k = c * y with 0 < k < n, then W embeds into the proper subfield fixed by the k-th power of Frobenius.

structure Cslib.CoeffPattern {F : Type u_1} [Field F] (n d : ℕ) [NeZero n] (a : ZMod n → F) : Prop

The zero pattern of the coefficient vector a of an image-subspace polynomial of a d-dimensional subspace that lies in no multiple of a proper subfield [BenSassonKopparty2012, Lemma 3.10]: the leading coefficient sits at n - d, the d - 1 positions above it vanish, the constant coefficient is nonzero, and every window of d - 1 consecutive positions starting in [1, n - d] meets a nonzero coefficient.

• le : d ≤ n

  The dimension is at most the degree of the field.

• lead : a ↑(n - d) ≠ 0

  The leading coefficient sits at position n - d.

• canonical (c : ℕ) : 1 ≤ c → c < d → a ↑(n - d + c) = 0

  The d - 1 positions above the leading one vanish.

• zero_ne : a 0 ≠ 0

  The constant coefficient is nonzero.

• gap (ρ : ℕ) : 1 ≤ ρ → ρ + d ≤ n → ∃ c < d - 1, a ↑(ρ + c) ≠ 0

  Every window of d - 1 consecutive positions starting in [1, n - d] meets a nonzero coefficient.

theorem Cslib.exists_coeffPattern {F : Type u_1} [Field F] [Algebra (ZMod 2) F] [Finite F] {n s : ℕ} [NeZero n] (hn : Module.finrank (ZMod 2) F = n) (hs : ∀ (K : Subfield F), K ≠ ⊤ → Nat.card ↥K ≤ 2 ^ s) (W : Submodule (ZMod 2) F) (hsW : s < Module.finrank (ZMod 2) ↥W) : ∃ (a : ZMod n → F), (∀ (x : F), linearizedEval a x ∈ W) ∧ CoeffPattern n (Module.finrank (ZMod 2) ↥W) a

Structural lemma [BenSassonKopparty2012, Lemma 3.10], for subspaces larger than every proper subfield: a subspace W of dimension greater than s, where every proper subfield has at most 2 ^ s elements, is the image of a linearized function whose coefficient vector has the zero pattern CoeffPattern.