Explicit binary fields of composite degree

For distinct primes mᵢ with product n, each least-code irreducible binary polynomial Cslib.leastIrreducible mᵢ has a root αᵢ in 𝔽_{2 ^ n} = GaloisField 2 n (Cslib.AffineDisperser.binaryRoot), and the monomials ∏ᵢ αᵢ ^ Jᵢ, Jᵢ < mᵢ, form a basis of 𝔽_{2 ^ n} over 𝔽₂ (Cslib.AffineDisperser.compositeBasis). Arithmetic in this basis is arithmetic in 𝔽₂[X₁, …, Xₖ] / (g₁(X₁), …, gₖ(Xₖ)), which needs only the polynomials of small degree mᵢ.

Main definitions

• Cslib.AffineDisperser.binaryRoot: a root of leastIrreducible p in GaloisField 2 n, p ∣ n.
• Cslib.AffineDisperser.compositeBasis: the monomial basis of GaloisField 2 (∏ᵢ mᵢ) for distinct primes mᵢ.

Main results

• Cslib.AffineDisperser.exists_aeval_leastIrreducible_eq_zero: leastIrreducible p has a root in GaloisField 2 n when p ∣ n.
• Cslib.AffineDisperser.minpoly_binaryRoot: when p ∣ n and p, n ≠ 0, the minimal polynomial of binaryRoot p n over 𝔽₂ is leastIrreducible p.

References

• R. Lidl, H. Niederreiter, Finite Fields, Chapters 1 and 3

theorem Cslib.AffineDisperser.exists_aeval_leastIrreducible_eq_zero {p n : ℕ} (hp : p ≠ 0) (hn : n ≠ 0) (hpn : p ∣ n) : ∃ (α : GaloisField 2 n), (Polynomial.aeval α) (leastIrreducible p) = 0

leastIrreducible p has a root in 𝔽_{2 ^ n} when p ∣ n.

noncomputable def Cslib.AffineDisperser.binaryRoot (p n : ℕ) : GaloisField 2 n

A root of leastIrreducible p in 𝔽_{2 ^ n}, which exists when p ∣ n and p, n ≠ 0 (0 when there is none). The root is chosen arbitrarily; the explicit disperser does not depend on the choice (Cslib.AffineDisperser.traceSymBits_rootBasis_eq_explicitDisperser).

theorem Cslib.AffineDisperser.minpoly_binaryRoot {p n : ℕ} (hp : p ≠ 0) (hn : n ≠ 0) (hpn : p ∣ n) : minpoly (ZMod 2) (binaryRoot p n) = leastIrreducible p

When p ∣ n and p, n ≠ 0, the minimal polynomial of binaryRoot p n over 𝔽₂ is leastIrreducible p.

noncomputable def Cslib.AffineDisperser.compositeBasis {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : ι → ℕ) (hm : ∀ (i : ι), Nat.Prime (m i)) (hinj : Function.Injective m) : Module.Basis ((i : ι) → Fin (m i)) (ZMod 2) (GaloisField 2 (∏ i : ι, m i))

The monomial basis of 𝔽_{2 ^ n}, n = ∏ᵢ mᵢ for distinct primes mᵢ: the monomials ∏ᵢ αᵢ ^ Jᵢ, Jᵢ < mᵢ, in roots αᵢ = binaryRoot mᵢ n of the irreducible polynomials leastIrreducible mᵢ.

theorem Cslib.AffineDisperser.compositeBasis_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : ι → ℕ) (hm : ∀ (i : ι), Nat.Prime (m i)) (hinj : Function.Injective m) (J : (i : ι) → Fin (m i)) : (compositeBasis m hm hinj) J = ∏ i : ι, binaryRoot (m i) (∏ i : ι, m i) ^ ↑(J i)

The basis vector of compositeBasis at exponents J is the monomial ∏ᵢ αᵢ ^ Jᵢ in the roots αᵢ = binaryRoot mᵢ (∏ᵢ mᵢ).