Explicit binary fields of every degree

A binary polynomial is coded by the natural number whose binary digits, least significant first, are its coefficients (Cslib.polyOfCode). The irreducible polynomial of degree w with the least code (Cslib.leastIrreducible) is found by exhaustive search through the 2 ^ w codes in [2 ^ w, 2 ^ (w + 1)) (Cslib.exists_code_leastIrreducible).

Cslib.BinaryField w is the field 𝔽₂[X] / (g) for g = Cslib.leastIrreducible w. For w ≠ 0 its power basis 1, α, …, α ^ (w - 1) at the root α of g (Cslib.BinaryField.basis) encodes its elements by w bits via an additive equivalence (Cslib.BinaryField.equivBits), so it has 2 ^ w elements (Cslib.BinaryField.card); the class of a binary polynomial of degree less than w is encoded by its coefficients (Cslib.BinaryField.equivBits_mk). Bit strings of length b ≤ w embed as the polynomials of degree less than b (Cslib.BinaryField.embed).

The modulus is explicit: its code is the least code of an irreducible binary polynomial of degree w, which is computed by trial division (Cslib.AffineDisperser.leastIrreducibleCode), so the field arithmetic is a computation on bit strings. This is why the field is the quotient AdjoinRoot g rather than Mathlib's GaloisField 2 w: the splitting field of X ^ (2 ^ w) - X comes with no basis. In AdjoinRoot g the power basis is the coefficient list itself, for every degree w.

For w = 0 the modulus is X and the field has two elements; the basis and the encoding by bits need w ≠ 0.

Main definitions

• Cslib.polyOfCode: the binary polynomial with a given code.
• Cslib.leastIrreducible: the irreducible binary polynomial of degree w with the least code (X when w = 0).
• Cslib.BinaryField: the explicit binary field of degree w.
• Cslib.BinaryField.basis: its power basis over 𝔽₂.
• Cslib.BinaryField.equivBits: its additive equivalence with BitString w.
• Cslib.BinaryField.embed: the embedding of bit strings of length b ≤ w.

Main results

• Cslib.irreducible_leastIrreducible, Cslib.monic_leastIrreducible, Cslib.natDegree_leastIrreducible: leastIrreducible w is monic and irreducible, of degree w when w ≠ 0.
• Cslib.exists_code_leastIrreducible: the code of leastIrreducible p lies in [2 ^ p, 2 ^ (p + 1)), and no smaller code is irreducible of degree p.
• Cslib.BinaryField.card: the field has 2 ^ w elements.
• Cslib.BinaryField.equivBits_mk: the encoding of a polynomial of degree less than w is its list of coefficients.

References

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

@[irreducible]

noncomputable def Cslib.polyOfCode (m : ℕ) : Polynomial (ZMod 2)

The binary polynomial whose coefficients, from the constant term up, are the binary digits of m, least significant first.

@[simp]

theorem Cslib.polyOfCode_zero : polyOfCode 0 = 0

The code 0 gives the zero polynomial.

theorem Cslib.polyOfCode_two_mul_add (m : ℕ) (b : ZMod 2) : polyOfCode (2 * m + b.val) = Polynomial.C b + Polynomial.X * polyOfCode m

Appending the bit b below the code m multiplies by X and adds the constant b.

theorem Cslib.polyOfCode_ne_zero_and_natDegree {m : ℕ} (hm : m ≠ 0) : polyOfCode m ≠ 0 ∧ (polyOfCode m).natDegree = Nat.log 2 m

The code m ≠ 0 gives a nonzero polynomial of degree ⌊log₂ m⌋.

theorem Cslib.natDegree_polyOfCode {m : ℕ} (hm : m ≠ 0) : (polyOfCode m).natDegree = Nat.log 2 m

The code m ≠ 0 gives a polynomial of degree ⌊log₂ m⌋.

theorem Cslib.polyOfCode_surjective : Function.Surjective polyOfCode

Every binary polynomial has a code.

theorem Cslib.exists_irreducible_natDegree_eq {p : ℕ} (hp : p ≠ 0) : ∃ (g : Polynomial (ZMod 2)), Irreducible g ∧ g.natDegree = p

There is an irreducible binary polynomial of every positive degree p: the minimal polynomial of a primitive element of 𝔽_{2 ^ p}.

noncomputable def Cslib.leastIrreducible (p : ℕ) : Polynomial (ZMod 2)

The irreducible binary polynomial of degree p with the least code (X when p = 0, where no irreducible polynomial exists).

theorem Cslib.leastIrreducible_zero : leastIrreducible 0 = Polynomial.X

The least irreducible binary polynomial of degree zero is X, by the convention of Cslib.leastIrreducible.

theorem Cslib.irreducible_leastIrreducible (w : ℕ) : Irreducible (leastIrreducible w)

leastIrreducible w is irreducible for every degree w, including w = 0.

theorem Cslib.natDegree_leastIrreducible {p : ℕ} (hp : p ≠ 0) : (leastIrreducible p).natDegree = p

For p ≠ 0, leastIrreducible p has degree p.

theorem Cslib.exists_code_leastIrreducible {p : ℕ} (hp : p ≠ 0) : ∃ (m : ℕ), 2 ^ p ≤ m ∧ m < 2 ^ (p + 1) ∧ leastIrreducible p = polyOfCode m ∧ ∀ m' < m, ¬(Irreducible (polyOfCode m') ∧ (polyOfCode m').natDegree = p)

The exhaustive search: leastIrreducible p is polyOfCode m for a code 2 ^ p ≤ m < 2 ^ (p + 1) such that no smaller code is irreducible of degree p.

theorem Cslib.monic_leastIrreducible (w : ℕ) : (leastIrreducible w).Monic

leastIrreducible w is monic for every degree w, as every nonzero binary polynomial is.

@[reducible, inline]

abbrev Cslib.BinaryField (w : ℕ) : Type

The explicit binary field of degree w: binary polynomials modulo the irreducible polynomial of degree w with the least code.

instance Cslib.BinaryField.instFactIrreduciblePolynomialZModOfNatNatLeastIrreducible (w : ℕ) : Fact (Irreducible (leastIrreducible w))

The modulus is irreducible, so the quotient is a field.

@[instance_reducible]

noncomputable instance Cslib.BinaryField.instField (w : ℕ) : Field (BinaryField w)

The explicit binary field is a field.

@[instance_reducible]

noncomputable instance Cslib.BinaryField.instFintype (w : ℕ) : Fintype (BinaryField w)

The explicit binary field is finite, through its coordinates in the power basis.

@[instance_reducible]

noncomputable instance Cslib.BinaryField.instDecidableEq (w : ℕ) : DecidableEq (BinaryField w)

Equality in the explicit binary field, decided classically.

instance Cslib.BinaryField.instCharPOfNatNat (w : ℕ) : CharP (BinaryField w) 2

The explicit binary field has characteristic two.

noncomputable def Cslib.BinaryField.basis {w : ℕ} (hw : w ≠ 0) : Module.Basis (Fin w) (ZMod 2) (BinaryField w)

The power basis 1, α, …, α ^ (w - 1) at the root α of the modulus, for w ≠ 0.

theorem Cslib.BinaryField.basis_apply {w : ℕ} (hw : w ≠ 0) (i : Fin w) : (basis hw) i = AdjoinRoot.root (leastIrreducible w) ^ ↑i

The basis vector i is the power α ^ i of the root.

noncomputable def Cslib.BinaryField.equivBits {w : ℕ} (hw : w ≠ 0) : BinaryField w ≃+ BitString w

The encoding by bits: the w coordinates in the power basis, for w ≠ 0, as an additive equivalence BinaryField w ≃+ BitString w.

theorem Cslib.BinaryField.equivBits_apply {w : ℕ} (hw : w ≠ 0) (x : BinaryField w) (j : Fin w) : (equivBits hw) x j = BitString.bitEquiv (((basis hw).repr x) j)

Bit j of an element is its coordinate j in the power basis.

theorem Cslib.BinaryField.equivBits_symm_apply {w : ℕ} (hw : w ≠ 0) (v : BitString w) : (equivBits hw).symm v = ∑ j : Fin w, BitString.bitEquiv.symm (v j) • (basis hw) j

The element with given bits is the combination of the basis vectors selected by the bits.

theorem Cslib.BinaryField.card {w : ℕ} (hw : w ≠ 0) : Fintype.card (BinaryField w) = 2 ^ w

The explicit binary field of degree w ≠ 0 has 2 ^ w elements.

theorem Cslib.BinaryField.equivBits_mk {w : ℕ} (hw : w ≠ 0) {p : Polynomial (ZMod 2)} (hp : p.degree < ↑w) (j : Fin w) : (equivBits hw) ((AdjoinRoot.mk (leastIrreducible w)) p) j = BitString.bitEquiv (p.coeff ↑j)

The encoding of the class of a binary polynomial of degree less than w is its list of coefficients.

noncomputable def Cslib.BinaryField.embed {w b : ℕ} (hw : w ≠ 0) (hbw : b ≤ w) : BitString b ↪ BinaryField w

The embedding of bit strings of length b ≤ w: a bit string is the polynomial with these coefficients, padded with zeros to length w.

theorem Cslib.BinaryField.embed_apply {w b : ℕ} (hw : w ≠ 0) (hbw : b ≤ w) (a : BitString b) : (embed hw hbw) a = (equivBits hw).symm fun (j : Fin w) => if h : ↑j < b then a ⟨↑j, h⟩ else false

The embedded bit string is the element whose bits are those of the string, padded with zeros.