Subfields of finite binary fields and additive bit-string encodings

A proper subfield K of a finite field F has degree [F : K] ≥ 2, so |K| ^ 2 ≤ |F| (Cslib.card_sq_le_of_ne_top). When F has 2 ^ n elements and every prime factor of n exceeds L, the degree [F : K] is at least L + 1, so |K| ≤ 2 ^ (n / (L + 1)) (Cslib.card_subfield_le_of_lt_prime), and in particular |K| ≤ 2 ^ (n / 2) for every proper subfield (Cslib.card_subfield_le).

Every finite field K of characteristic two with 2 ^ b elements is a b-dimensional vector space over ZMod 2; coordinates in a basis identify its additive group with BitString b, whose addition is coordinatewise exclusive or (Cslib.nonempty_addEquiv_bitString). Fields of characteristic two with 2 ^ n elements exist for every n ≠ 0 (Cslib.exists_field_card_eq_two_pow).

Main results

• Cslib.card_sq_le_of_ne_top: a proper subfield K of a finite field F satisfies |K| ^ 2 ≤ |F|.
• Cslib.card_subfield_le_of_lt_prime: if every prime factor of n exceeds L, every proper subfield of a field with 2 ^ n elements has at most 2 ^ (n / (L + 1)) elements.
• Cslib.card_subfield_le: every proper subfield of a field with 2 ^ n elements has at most 2 ^ (n / 2) elements.
• Cslib.nonempty_addEquiv_bitString: a field of characteristic two with 2 ^ b elements is additively equivalent to BitString b.
• Cslib.exists_field_card_eq_two_pow: there is a field of characteristic two with 2 ^ n elements for every n ≠ 0.

References

• R. Lidl, H. Niederreiter, Finite Fields, Chapter 2
• E. Ben-Sasson, S. Kopparty, Affine dispersers from subspace polynomials
• Adapted from MassProduction/BinaryField.lean in S. Schlesinger, Boolean circuit mass production formalization.

theorem Cslib.card_sq_le_of_ne_top {F : Type u_1} [Field F] [Finite F] {K : Subfield F} (hK : K ≠ ⊤) : Nat.card ↥K ^ 2 ≤ Nat.card F

A proper subfield K of a finite field F satisfies |K| ^ 2 ≤ |F|.

instance Cslib.charP_two_of_algebra_zmod_two (R : Type u_2) [Ring R] [Nontrivial R] [Algebra (ZMod 2) R] : CharP R 2

A nontrivial 𝔽₂-algebra has characteristic two.

theorem Cslib.card_subfield_le_of_lt_prime {F : Type u_1} [Field F] [Finite F] [Algebra (ZMod 2) F] {n L : ℕ} (hn : Module.finrank (ZMod 2) F = n) (hL : ∀ (q : ℕ), Nat.Prime q → q ∣ n → L < q) (K : Subfield F) (hK : K ≠ ⊤) : Nat.card ↥K ≤ 2 ^ (n / (L + 1))

Subfields of 𝔽_{2 ^ n}: if every prime factor of n exceeds L, every proper subfield of a field with 2 ^ n elements has at most 2 ^ (n / (L + 1)) elements.

theorem Cslib.card_subfield_le {F : Type u_1} [Field F] [Finite F] [Algebra (ZMod 2) F] {n : ℕ} (hn : Module.finrank (ZMod 2) F = n) (K : Subfield F) (hK : K ≠ ⊤) : Nat.card ↥K ≤ 2 ^ (n / 2)

In a field with 2 ^ n elements every proper subfield has at most 2 ^ (n / 2) elements.

theorem Cslib.nonempty_addEquiv_bitString {K : Type u_2} [Field K] [Fintype K] [CharP K 2] {b : ℕ} (hK : Fintype.card K = 2 ^ b) : Nonempty (K ≃+ BitString b)

A field of characteristic two with 2 ^ b elements is additively equivalent to BitString b, whose addition is coordinatewise exclusive or.

theorem Cslib.exists_field_card_eq_two_pow {n : ℕ} (hn : n ≠ 0) : ∃ (K : Type) (x : Field K) (x_1 : Fintype K), CharP K 2 ∧ Fintype.card K = 2 ^ n

For every n ≠ 0 there is a field of characteristic two with exactly 2 ^ n elements, for example the Galois field GaloisField 2 n.