Algebra & fields

GF(4): build an extension field

Construct a Galois field yourself, then let Lean exhaustively verify its addition, multiplication, and inverses.

-- GF(4): build an extension field
-- History: 2001 · AES standard: a larger binary-field application.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Four elements need two bits, but GF(4) is not arithmetic modulo 4. Here u²=u+1.
-- Scope: Defines GF(2)[u]/(u²+u+1) as two binary coefficients and checks all field laws. This is a small teaching field; AES instead uses GF(256).
-- Source: https://csrc.nist.gov/pubs/fips/197/final

-- (a,b) represents a+b*u; coefficients live modulo 2.
abbrev F4 := Fin 2 × Fin 2

-- Teach decide to enumerate both binary coefficients.
instance (P : F4 → Prop) [DecidablePred P] : Decidable (∀ x, P x) :=
  decidable_of_iff (∀ a b : Fin 2, P (a,b))
    ⟨fun h x => h x.1 x.2, fun h a b => h (a,b)⟩
instance (P : F4 → Prop) [DecidablePred P] : Decidable (∃ x, P x) :=
  decidable_of_iff (∃ a b : Fin 2, P (a,b))
    ⟨fun ⟨a,b,h⟩ => ⟨(a,b),h⟩, fun ⟨(a,b),h⟩ => ⟨a,b,h⟩⟩

def add (x y : F4) : F4 := (x.1+y.1, x.2+y.2)
-- Reduce u² to u+1 after multiplying the polynomials.
def mul (x y : F4) : F4 :=
  (x.1*y.1+x.2*y.2, x.1*y.2+x.2*y.1+x.2*y.2)

def zero : F4 := (0,0)
def one : F4 := (1,0)
def u : F4 := (0,1)

example : ∀ a b c : F4, add (add a b) c = add a (add b c) := by decide
example : ∀ a b : F4, add a b = add b a := by decide
example : ∀ a : F4, add a zero = a ∧ add a a = zero := by decide
example : ∀ a b c : F4, mul (mul a b) c = mul a (mul b c) := by decide
example : ∀ a b : F4, mul a b = mul b a := by decide
example : ∀ a : F4, mul a one = a := by decide
example : ∀ a b c : F4, mul a (add b c) = add (mul a b) (mul a c) := by decide
example : zero ≠ one := by decide
example : ∀ a : F4, a ≠ zero → ∃ b : F4, mul a b = one := by decide

example : mul u u = add u one := by decide
#eval mul u (add u one)

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`decide`

Builds a proof using a decision procedure. Quantifying over Fin n checks every one of its finitely many values.

`Fin n`

Fin n contains the natural numbers less than n, each with a bound proof. Addition and multiplication wrap modulo n.

Background and proof scope

2001 · AES standard: a larger binary-field application

Four elements need two bits, but GF(4) is not arithmetic modulo 4. Here u²=u+1.

Defines GF(2)[u]/(u²+u+1) as two binary coefficients and checks all field laws. This is a small teaching field; AES instead uses GF(256).

NIST: AES and binary finite fields

Expected output

Reference only. Run the file to check its actual result.

(1, 0)

Exercise

Remove the x.2*y.2 contribution from the second coefficient. Which field laws break?