Explicit binary fields defined by irreducible trinomials

For every t : ℕ, the cyclotomic polynomial Φ_{3 ^ (t + 1)}(X) over 𝔽₂ = ZMod 2 is the explicit trinomial Cslib.trinomial t = X ^ (2 * 3 ^ t) + X ^ (3 ^ t) + 1. Because 2 is a primitive root modulo 3 ^ (t + 1) for every t (orderOf 2 = 2 * 3 ^ t), Cslib.trinomial t is irreducible over ZMod 2 (Cslib.irreducible_trinomial) Lidl and Niederreiter, Theorem 2.47.

Unlike Cslib.BinaryField w, whose modulus Cslib.leastIrreducible w is defined by an exhaustive search over binary codes, Cslib.TrinomialField t = AdjoinRoot (trinomial t) has a closed-form sparse modulus of degree 2 * 3 ^ t for every t : ℕ without any runtime polynomial search. Moreover, because (X ^ (3 ^ t) + 1) * trinomial t = X ^ (3 ^ (t + 1)) + 1 over ZMod 2, any binary polynomial of degree less than 4 * 3 ^ t (whose binary code below 2 ^ (4 * 3 ^ t) splits into four 3 ^ t-bit limbs, with the low two limbs kept together as a 2 * 3 ^ t-bit word) reduces modulo trinomial t in closed form using only bitwise shifts, masks, and exclusive-or (Cslib.reduceTrinomialCode, Cslib.mk_polyOfCode_reduceTrinomialCode). Paired with carryless multiplication Cslib.clmul (Cslib.polyOfCode_clmul), this gives loop-free arithmetic for Cslib.TrinomialField t on unsigned machine words.

Main definitions

• Cslib.trinomial: the binary trinomial X ^ (2 * 3 ^ t) + X ^ (3 ^ t) + 1.
• Cslib.clmul: carryless multiplication of natural-number polynomial codes over 𝔽₂.
• Cslib.reduceTrinomialCode: 4-limb bitwise reduction modulo trinomial t on natural-number codes below 2 ^ (4 * 3 ^ t) (four 3 ^ t-bit limbs).
• Cslib.TrinomialField: the explicit binary field AdjoinRoot (trinomial t) of degree 2 * 3 ^ t.
• Cslib.TrinomialField.basis, Cslib.TrinomialField.equivBits, Cslib.TrinomialField.equivFin, Cslib.TrinomialField.embed, Cslib.TrinomialField.embedFin: power basis, coordinate equivalences with BitString (2 * 3 ^ t) and Fin (2 ^ (2 * 3 ^ t)), and embeddings of bit strings and bounded natural indices.

Main results

• Cslib.trinomial_eq_cyclotomic, Cslib.monic_trinomial, Cslib.natDegree_trinomial, Cslib.irreducible_trinomial: trinomial t is the 3 ^ (t + 1)-th cyclotomic polynomial over ZMod 2, monic of degree 2 * 3 ^ t, and irreducible.
• Cslib.coeff_polyOfCode, Cslib.polyOfCode_injective, Cslib.polyOfCode_xor, Cslib.polyOfCode_shiftLeft, Cslib.polyOfCode_eq_and_add_shiftRight: bit-level correspondence between polyOfCode and bitwise operations on ℕ.
• Cslib.polyOfCode_clmul, Cslib.clmul_lt_two_pow: clmul computes polynomial multiplication over ZMod 2 and respects bit-width bounds.
• Cslib.reduceTrinomialCode_lt, Cslib.mk_polyOfCode_reduceTrinomialCode: reduceTrinomialCode produces a < 2 ^ (2 * 3 ^ t) code congruent modulo trinomial t.
• Cslib.TrinomialField.card, Cslib.TrinomialField.val_equivFin_add, Cslib.TrinomialField.val_equivFin_mul: cardinality and unsigned-word arithmetic laws of TrinomialField t.

References

• R. Lidl, H. Niederreiter, Finite Fields, Section 2.4 and Chapter 3

Irreducibility of X ^ (2 * 3 ^ t) + X ^ (3 ^ t) + 1 over ZMod 2

noncomputable def Cslib.trinomial (t : ℕ) : Polynomial (ZMod 2)

The binary trinomial X ^ (2 * 3 ^ t) + X ^ (3 ^ t) + 1 of degree 2 * 3 ^ t over ZMod 2.

theorem Cslib.trinomial_eq_cyclotomic (t : ℕ) : trinomial t = Polynomial.cyclotomic (3 ^ (t + 1)) (ZMod 2)

trinomial t is the 3 ^ (t + 1)-th cyclotomic polynomial over ZMod 2.

theorem Cslib.monic_trinomial (t : ℕ) : (trinomial t).Monic

trinomial t is monic for every t : ℕ.

theorem Cslib.natDegree_trinomial (t : ℕ) : (trinomial t).natDegree = 2 * 3 ^ t

trinomial t has degree 2 * 3 ^ t.

theorem Cslib.mul_trinomial_eq (t : ℕ) : (Polynomial.X ^ 3 ^ t + 1) * trinomial t = Polynomial.X ^ 3 ^ (t + 1) + 1

Over ZMod 2, multiplying trinomial t by X ^ (3 ^ t) + 1 yields X ^ (3 ^ (t + 1)) + 1.

theorem Cslib.orderOf_two_zmod_three_pow (t : ℕ) : orderOf 2 = 2 * 3 ^ t

The multiplicative order of 2 modulo 3 ^ (t + 1) is 2 * 3 ^ t.

theorem Cslib.irreducible_trinomial (t : ℕ) : Irreducible (trinomial t)

trinomial t is irreducible over ZMod 2 for every t : ℕ Lidl and Niederreiter, Theorem 2.47.

Bitwise operations, carryless multiplication, and 4-limb reduction on polyOfCode

theorem Cslib.polyOfCode_eq_C_add_X_mul (m : ℕ) : polyOfCode m = Polynomial.C ↑m + Polynomial.X * polyOfCode (m / 2)

Unfolding polyOfCode m into its constant term m : ZMod 2 and X * polyOfCode (m / 2).

theorem Cslib.coeff_polyOfCode (m i : ℕ) : (polyOfCode m).coeff i = BitString.bitEquiv.symm (m.testBit i)

Coefficient i of polyOfCode m is bit i of m read in ZMod 2.

theorem Cslib.polyOfCode_injective : Function.Injective polyOfCode

polyOfCode is injective: distinct natural numbers have distinct binary polynomials.

theorem Cslib.degree_polyOfCode_lt {m k : ℕ} (hm : m < 2 ^ k) : (polyOfCode m).degree < ↑k

If m < 2 ^ k, then polyOfCode m has degree strictly less than k.

@[simp]

theorem Cslib.polyOfCode_xor (a b : ℕ) : polyOfCode (a ^^^ b) = polyOfCode a + polyOfCode b

Bitwise exclusive-or on codes corresponds to polynomial addition over ZMod 2.

@[simp]

theorem Cslib.polyOfCode_shiftLeft (a k : ℕ) : polyOfCode (a <<< k) = Polynomial.X ^ k * polyOfCode a

Left-shifting a code by k bits multiplies its polynomial by X ^ k.

theorem Cslib.polyOfCode_eq_and_add_shiftRight (a k : ℕ) : polyOfCode a = polyOfCode (a &&& 2 ^ k - 1) + Polynomial.X ^ k * polyOfCode (a >>> k)

Splitting a code at bit k into its low k bits (a &&& (2 ^ k - 1)) and high bits (a >>> k).

@[irreducible]

def Cslib.clmul (a b : ℕ) : ℕ

Carryless multiplication of natural-number polynomial codes over ZMod 2.

@[simp]

theorem Cslib.clmul_zero_right (a : ℕ) : clmul a 0 = 0

Carryless multiplication by 0 on the right is 0.

theorem Cslib.clmul_step (a b : ℕ) : clmul a b = (if b &&& 1 = 1 then a else 0) ^^^ clmul a (b >>> 1) <<< 1

Step equation for clmul in terms of bitwise shift and mask.

@[simp]

theorem Cslib.polyOfCode_clmul (a b : ℕ) : polyOfCode (clmul a b) = polyOfCode a * polyOfCode b

clmul computes polynomial multiplication over ZMod 2.

@[simp]

theorem Cslib.clmul_zero_left (b : ℕ) : clmul 0 b = 0

Carryless multiplication by 0 on the left is 0.

theorem Cslib.clmul_comm (a b : ℕ) : clmul a b = clmul b a

Carryless multiplication is commutative.

theorem Cslib.clmul_xor_left (a b c : ℕ) : clmul (a ^^^ b) c = clmul a c ^^^ clmul b c

Carryless multiplication distributes over ^^^ on the left.

theorem Cslib.clmul_xor_right (a b c : ℕ) : clmul a (b ^^^ c) = clmul a b ^^^ clmul a c

Carryless multiplication distributes over ^^^ on the right.

theorem Cslib.clmul_shiftLeft_left (a b k : ℕ) : clmul (a <<< k) b = clmul a b <<< k

Carryless multiplication commutes with left shifts on the left.

theorem Cslib.clmul_shiftLeft_right (a b k : ℕ) : clmul a (b <<< k) = clmul a b <<< k

Carryless multiplication commutes with left shifts on the right.

theorem Cslib.clmul_lt_two_pow {a b m n : ℕ} (ha : a < 2 ^ m) (hb : b < 2 ^ n) : clmul a b < 2 ^ (m + n)

If a < 2 ^ m and b < 2 ^ n, then clmul a b < 2 ^ (m + n).

theorem Cslib.clmul_lt_two_pow_two_mul {a b q : ℕ} (ha : a < 2 ^ q) (hb : b < 2 ^ q) : clmul a b < 2 ^ (2 * q)

If a < 2 ^ q and b < 2 ^ q, then clmul a b < 2 ^ (2 * q).

def Cslib.reduceTrinomialCode (t c : ℕ) : ℕ

8-operation loop-free 4-limb reduction modulo trinomial t: viewing a code c < 2 ^ (4 * 3 ^ t) as four 3 ^ t-bit limbs (with the low two limbs kept together as cLow), reduces c to a code < 2 ^ (2 * 3 ^ t) representing the same element of AdjoinRoot (trinomial t).

theorem Cslib.reduceTrinomialCode_lt (t : ℕ) {c : ℕ} (hc : c < 2 ^ (4 * 3 ^ t)) : reduceTrinomialCode t c < 2 ^ (2 * 3 ^ t)

For c < 2 ^ (4 * 3 ^ t), reduceTrinomialCode t c < 2 ^ (2 * 3 ^ t).

theorem Cslib.mk_polyOfCode_reduceTrinomialCode (t c : ℕ) : (AdjoinRoot.mk (trinomial t)) (polyOfCode (reduceTrinomialCode t c)) = (AdjoinRoot.mk (trinomial t)) (polyOfCode c)

reduceTrinomialCode t c is congruent to c modulo trinomial t for every c : ℕ.

The explicit trinomial field TrinomialField t

@[reducible, inline]

abbrev Cslib.TrinomialField (t : ℕ) : Type

The explicit binary field of degree 2 * 3 ^ t: binary polynomials modulo trinomial t.

theorem Cslib.TrinomialField.deg_ne_zero (t : ℕ) : 2 * 3 ^ t ≠ 0

Degree 2 * 3 ^ t is always positive.

instance Cslib.TrinomialField.instFactIrreduciblePolynomialZModOfNatNatTrinomial (t : ℕ) : Fact (Irreducible (trinomial t))

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

@[instance_reducible]

noncomputable instance Cslib.TrinomialField.instField (t : ℕ) : Field (TrinomialField t)

TrinomialField t is a field.

@[instance_reducible]

noncomputable instance Cslib.TrinomialField.instFintype (t : ℕ) : Fintype (TrinomialField t)

TrinomialField t is finite, through its coordinates in the power basis.

@[instance_reducible]

noncomputable instance Cslib.TrinomialField.instDecidableEq (t : ℕ) : DecidableEq (TrinomialField t)

Equality in TrinomialField t, decided classically.

instance Cslib.TrinomialField.instCharPOfNatNat (t : ℕ) : CharP (TrinomialField t) 2

TrinomialField t has characteristic two.

noncomputable def Cslib.TrinomialField.basis (t : ℕ) : Module.Basis (Fin (2 * 3 ^ t)) (ZMod 2) (TrinomialField t)

The power basis 1, α, …, α ^ (2 * 3 ^ t - 1) at the root α of trinomial t.

theorem Cslib.TrinomialField.basis_apply (t : ℕ) (i : Fin (2 * 3 ^ t)) : (basis t) i = AdjoinRoot.root (trinomial t) ^ ↑i

Basis vector i is the power α ^ i of the root.

noncomputable def Cslib.TrinomialField.equivBits (t : ℕ) : TrinomialField t ≃+ BitString (2 * 3 ^ t)

The encoding by bits: the 2 * 3 ^ t coordinates in the power basis as an additive equivalence TrinomialField t ≃+ BitString (2 * 3 ^ t).

theorem Cslib.TrinomialField.equivBits_apply (t : ℕ) (x : TrinomialField t) (j : Fin (2 * 3 ^ t)) : (equivBits t) x j = BitString.bitEquiv (((basis t).repr x) j)

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

theorem Cslib.TrinomialField.equivBits_symm_apply (t : ℕ) (v : BitString (2 * 3 ^ t)) : (equivBits t).symm v = ∑ j : Fin (2 * 3 ^ t), BitString.bitEquiv.symm (v j) • (basis t) j

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

theorem Cslib.TrinomialField.card (t : ℕ) : Fintype.card (TrinomialField t) = 2 ^ (2 * 3 ^ t)

TrinomialField t has 2 ^ (2 * 3 ^ t) elements.

theorem Cslib.TrinomialField.equivBits_mk (t : ℕ) {p : Polynomial (ZMod 2)} (hp : p.degree < ↑(2 * 3 ^ t)) (j : Fin (2 * 3 ^ t)) : (equivBits t) ((AdjoinRoot.mk (trinomial t)) p) j = BitString.bitEquiv (p.coeff ↑j)

The encoding of the class of a binary polynomial of degree less than 2 * 3 ^ t is its list of coefficients.

noncomputable def Cslib.TrinomialField.equivFin (t : ℕ) : TrinomialField t ≃ Fin (2 ^ (2 * 3 ^ t))

Numbering of TrinomialField t by Fin (2 ^ (2 * 3 ^ t)) via its power-basis bits.

theorem Cslib.TrinomialField.val_equivFin_mk_polyOfCode (t : ℕ) {c : ℕ} (hc : c < 2 ^ (2 * 3 ^ t)) : ↑((equivFin t) ((AdjoinRoot.mk (trinomial t)) (polyOfCode c))) = c

For c < 2 ^ (2 * 3 ^ t), the equivFin t coordinate of AdjoinRoot.mk (trinomial t) (polyOfCode c) is c.

theorem Cslib.TrinomialField.equivFin_symm_eq_mk_polyOfCode (t : ℕ) (m : Fin (2 ^ (2 * 3 ^ t))) : (equivFin t).symm m = (AdjoinRoot.mk (trinomial t)) (polyOfCode ↑m)

The inverse of equivFin t sends m : Fin (2 ^ (2 * 3 ^ t)) to AdjoinRoot.mk (trinomial t) (polyOfCode m.val).

theorem Cslib.TrinomialField.mk_polyOfCode_val_equivFin (t : ℕ) (x : TrinomialField t) : (AdjoinRoot.mk (trinomial t)) (polyOfCode ↑((equivFin t) x)) = x

Every x : TrinomialField t is the class of polyOfCode (equivFin t x).val.

theorem Cslib.TrinomialField.val_equivFin_add (t : ℕ) (x y : TrinomialField t) : ↑((equivFin t) (x + y)) = ↑((equivFin t) x) ^^^ ↑((equivFin t) y)

Addition in TrinomialField t corresponds to bitwise exclusive-or (^^^) on equivFin t coordinates.

theorem Cslib.TrinomialField.val_equivFin_mul (t : ℕ) (x y : TrinomialField t) : ↑((equivFin t) (x * y)) = reduceTrinomialCode t (clmul ↑((equivFin t) x) ↑((equivFin t) y))

Multiplication in TrinomialField t corresponds to carryless multiplication clmul followed by 4-limb reduction reduceTrinomialCode on equivFin t coordinates.

noncomputable def Cslib.TrinomialField.embed {t b : ℕ} (hb : b ≤ 2 * 3 ^ t) : BitString b ↪ TrinomialField t

The embedding of bit strings of length b ≤ 2 * 3 ^ t into TrinomialField t.

noncomputable def Cslib.TrinomialField.embedFin {t U : ℕ} (hU : U ≤ 2 ^ (2 * 3 ^ t)) : Fin U ↪ TrinomialField t

The embedding of keys Fin U (U ≤ 2 ^ (2 * 3 ^ t)) into TrinomialField t.

theorem Cslib.TrinomialField.embedFin_apply {t U : ℕ} (hU : U ≤ 2 ^ (2 * 3 ^ t)) (u : Fin U) : (embedFin hU) u = (AdjoinRoot.mk (trinomial t)) (polyOfCode ↑u)

Applying embedFin hU to u : Fin U gives AdjoinRoot.mk (trinomial t) (polyOfCode u.val).