Formalisation of AKS Primality lemma

Stream: new members

[metakuntyyy]

Greetings, I am working on formalising AKS lemma. My blueprint is https://www3.nd.edu/~andyp/notes/AKS.pdf
I would need several theorems regarding the algebraic closure of the Galois field.

For now I was trying to play with polynomials a bit

import Mathlib


#check GaloisField 2 2

example ( a : GaloisField 2 2) : ( a + a = 0 ) := by
  exact CharTwo.add_self_eq_zero a



open Polynomial
open scoped Polynomial

example (p: ℤ[X]) (h: X^2+X+1 = p) : p.eval 1 = 3 :=by
  conv =>
    lhs
    rhs
    rw[← h]
  have hh: ((X^2+X+1):ℤ[X]).eval 1 = (1^2+1+1) := by sorry
  have d : (1^2+1+1) = (3:ℤ) := by decide
  rw[d] at hh
  exact hh

However something seemed wrong. Polynomial evaluation for some reason is noncomputable.

The author lifts for some reason everything to the closure of the finite field. Now I would need the minimal set of theorems that are interested for calculations in this field.

Here would be some needed theorems that I could crystallize:
For every r there exists a primitive r-th root of unity in the algebraic closure of $F_p$

How would I define this map Ψ : (Z/n)[x]/(x^r − 1) → Fp. This seems to be the canonical isomorphism.
For example in (Z/6)(X^12-1) the image of X^10 would get mapped to X^10 in F_2. There are 6^12 elements in the domain but I wonder what the reduction in the closure is. However there is not a specific element I can construct. The field is finite, there must be a way to give a element form of F_p.

What do I mean by that, clearly (5: Nat ), ( X-1 : Nat[X]) ( ?????? : AlgebraicClosure of F_p)

How do the elements look like and are there any simple examples I can study?

[Daniel Weber]

There is docs#AdjoinRoot, does it seem relevant? Computability of polynomials is indeed a problem, see https://github.com/leanprover-community/mathlib4/wiki/Computation-models-for-polynomials-and-finitely-supported-functions

[metakuntyyy]

Well it appears that simp can close some goals. I guess if in doubt try simp.

Here is something that I am trying now.

import Mathlib


#check GaloisField 2 2

example ( a : GaloisField 2 2) : ( a + a = 0 ) := by
  exact CharTwo.add_self_eq_zero a

example  : (1 : GaloisField 2 2):= by
  sorry

This does not compile. I want to explicitly get some elements of the GaloisField 2 2 and so some calculations.
It should have the elements $0,1,\alpha,\alpha+1$ and I'd like to show that each of those elements is an element of GaloisField and I'd also like to show $\alpha*\alpha+1 = 1$

The reason this is true is that the multiplicative unit group is cyclic of order 3, which means that for any a,b not equal to 0 and 1 and $a\neq b$ we have $a*b=1$, since both a and b generate the group.

However I am struggling to even show that 1 is an element, let alone $\alpha$

[metakuntyyy]

Ah I made some progress, i should be able to prove this theorem, right?

import Mathlib



example  (a: GaloisField 2 2) (b: GaloisField 2 2) (h1: a ≠ 0) (h2: b≠0)
(h3:a≠1) (h4:b≠1)(h5:a≠b): a*b = 1:= by
  sorry

[Adam Topaz]

It looks like a correct statement to me!

[Adam Topaz]

BTW, if you want 1 in the finite field, just write 1 (assuming lean has some way to know what type to expect). So, for example, the following should work (using your imports)

example : GaloisField 2 2 := 1

[Adam Topaz]

What the first part is saying, example : GaloisField 2 2 is that some term of GaloisField 2 2 is expected. When you then write := 1, you're telling lean "the term in question is 1"

[metakuntyyy]

Ok cool, atleast some progress.

import Mathlib

example  (a: GaloisField 2 2) (b: GaloisField 2 2) (h1: a ≠ 0) (h2: b≠0)
(h3:a≠1) (h4:b≠1)(h5:a≠b): a*b = 1:= by
  sorry

noncomputable example : GaloisField 2 2 := 0
noncomputable example : GaloisField 2 2 := 1
noncomputable example : GaloisField 2 2 := x
noncomputable example : GaloisField 2 2 := x + 1

Now, the first two work, as expected, but I need to generate the last two elements of the Galois Field.
Since mathlib is sparse with examples there is no way for me to even know what those elements are.

Looking at the documentation the Galois Field 2 2 is the splitting field to the polynomial X^4-x. The irreducibles are X, X+1 and X^2+X+1. I want to construct the nontrivial elements of the field now.

[Adam Topaz]

What is x supposed to be?

[metakuntyyy]

Ah I just want to construct the other 2 nontrivial elements. It's supposed to be an element of $F_2[X]/(X^2+X+1)$

I don't know how to construct it since there are no examples in the library.

[Adam Topaz]

docs#GaloisField

[Adam Topaz]

Hmmm… do we have in mathlib the fact that finite subgroups of the units of a field are all cyclic?

[Adam Topaz]

In any case, it looks like the theory of finite fields needs a lot more work in mathlib

[metakuntyyy]

Again, I've read that and I still have no clue how to construct the elements, the best I could see is this https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/SplittingField/Construction.html#Polynomial.SplittingField
which has following equation.

• f.SplittingField = (MvPolynomial (Polynomial.SplittingFieldAux f.natDegree f) K ⧸ RingHom.ker (MvPolynomial.aeval id).toRingHom)
• But this appears not much of great use for me as of now, since I am missing a great deal of construction implementation details. I assume there are some proofs involved that would suit such a calculation, digging in those apis without a hint whether the path is correct or not is just not worth doing.

All I want is a simple calculation, I want to construct the two nontrivial elements of this Galois field, multiply them and show that they are equal to one. That shouldn't be that hard, on paper the proof is one line.
$\alpha * \alpha+1 =\alpha^2+\alpha$, now $\alpha^2=\alpha+1$, rewriting gives $\\alpha+1+\alpha$ which by field and mod 2 is equal to 1.

Can I somehow do this calculation?

[metakuntyyy]

I am really just happy to do some trivial calculations first to get familiar with those objects.

[Yakov Pechersky]

If I understand correctly, this is true for any two nontrivial elements, so why not start with

example (a b : GaloisField 2 2) (ha : a \ne 0) (hb : b \ne 0) : a * b = 1 := by sorry

[metakuntyyy]

No, $\alpha*\alpha= \alpha+1$ so the statement is false.

I literally want this one

import Mathlib

example : (3: ZMod 7)+(5 : ZMod 7) = (1 :ZMod 7 ) := rfl

Just a small and simple example of how to calculate in those rings. Here the rfl tactic already closes the goal, which makes sense. I want now to extend this finite field a little bit more and do some calculations there.

[Yakov Pechersky]

Sorry for my mistake, I meant a + b + a then...?

[metakuntyyy]

I think there is a misunderstanding, forget the theorem that I would like to show for now. I just want to construct the two nontrivial elements of GaloisField 2 2 and show that the product is 1. That's all. It's the simplest non-trivial finite field of dimension strictly greater than 1.

This is from Sage:

k = GF(4,'X')
for i,x in enumerate(k):  print("{} {}".format(i, x))
j = k.from_integer(2)
l = k.from_integer(3)
m = j*l
print("j={} l={} j*l=m={}".format(j,l,m))

This is its output

0 0
1 X
2 X + 1
3 1
j=X l=X + 1 j*l=m=1

This is the documentation:
https://doc.sagemath.org/html/en/reference/finite_rings/sage/rings/finite_rings/element_base.html

I've never worked with sage in my life and this took me 3 minutes, because there are some examples in the documentation. This is the user experience I desire from general products. Theorem provers are complex and hard, I understand, but they shouldn't be harder than necessary.
There is no example in the mathlib doc, which makes it excruciatingly difficult to even know where you are wrong.

In my point of view there should be something like a morphism from $(ZMod p) [X] \to GaloisField p n$ for every n where you can lift the elements in the polynomial ring to the GaloisField.

[Adam Topaz]

GaloisField 2 2 is defined as the splitting field of $X^4-X$ over ZMod 2. You can try to use the API for splitting fields to find elements in GaloisField 2 2, but this will be a bit challenging. There is no "canonical" element in $\mathbb{F}_{4}$ which deserves to be called x. This is a choice you have to make.

[Adam Topaz]

Constructing a ring hom from (ZMod p)[X] to GaloisField p n requires (and is equivalent to!) a choice of an element of GaloisField p n.

[Adam Topaz]

Unfortunately, with the way that GaloisFields are implemented, they're not suitable for actual calculations, so you can't expect rfl and/or decide to work.

[Adam Topaz]

Here is what you can do. First, show that $X^2 + X + 1$ is irreducible over ZMod 2, and show that it splits in GaloisField 2 2 (e.g. by showing that it divides X^4 - X, whose splitting field is GaloisField 2 2 by definition). Then you have to choose a root of $X^2 + X + 1$ in GaloisField 2 2 using, for example, Polynomial.rootOfSplits. This is an element which you can call alpha, if you wish, and it will satisfy the property you want.

[Adam Topaz]

I guess for the lemma you want to prove it's not even strictly necessary to prove that $X^2 + X + 1$ is irreducible, although if you want to show that $\mathbb{F}_2[\alpha] = \mathbb{F}_4$ later on, you would want that as well.

[Edward van de Meent]

Adam Topaz said:

Constructing a ring hom from (ZMod p)[X] to GaloisField p n requires (and is equivalent to!) a choice of an element of GaloisField p n.

although this indeed requires a choice, it is still in mathlib, i believe: If i recall correctly, we do have the proof that the finite fields are uniquely determined by their size, and equivalent to GaloisField...

[Edward van de Meent]

docs#GaloisField.equivZmodP

[Edward van de Meent]

docs#FiniteField.ringEquivOfCardEq

[Edward van de Meent]

basically, you could define your own (computable!!) structure, and run with it!

[Yaël Dillies]

Isn't the computable structure precisely docs#AdjoinRoot ?

[Yaël Dillies]

Well, modulo the fact that Polynomial currently isn't computable

[Edward van de Meent]

and the fact that it is a quotient...

[Daniel Weber]

Edward van de Meent said:

and the fact that it is a quotient...

Do quotients hurt computability?

[Henrik Böving]

Quotients do have computation rules associated with them.

[Yaël Dillies]

In theory, no. In practice, yes. Consider eg ℚ defined as a quotient of ℤ × ℤ. If you define addition as a / b + c / d = (a * d + b * c)/(b * d), then 1/2 + 1/2 + ... produces exponentially big terms in the number of terms

[Yaël Dillies]

To preserve reasonable performance, you would need to define a / b + c / d = ((a * d + b * c)/gcd(a * d + b * c, b * d))/((b * d)/gcd(a * d + b * c, b * d)), in which case it's not very clear what the quotient approach even brings you

[Edward van de Meent]

Henrik Böving said:

Quotients do have computation rules associated with them.

i thought it wasn't computable because it is defined using an axiom?

[Yaël Dillies]

It is a "computable axiom"

[Edward van de Meent]

(upon more careful reading of #tpil chapter 12, apparently indeed it isnt, but is defined internally by Lean. #tpil only likens it to being defined with the axiom keyword)

[Edward van de Meent]

sanity check that it indeed is separate:

#print Quot.sound -- axiom ....
#print Quot.lift -- Quotient primitive ...

[Adam Topaz]

Edward van de Meent said:

Adam Topaz said:

Constructing a ring hom from (ZMod p)[X] to GaloisField p n requires (and is equivalent to!) a choice of an element of GaloisField p n.

although this indeed requires a choice, it is still in mathlib, i believe: If i recall correctly, we do have the proof that the finite fields are uniquely determined by their size, and equivalent to GaloisField...

I don't understand what you mean... GaloisField p n is a (commutative) algebra over ZMod p, so to construct a map from (ZMod p)[X] to this algebra, you need to specify where X goes, so you need to choose some element of GaloisField p n. It would be even better if you knew how to choose an element which generates the field. But I don't see how to do this with the definitions you linked.

[Edward van de Meent]

first, you define an equivalent field which is completely computable and in which you know the generator, and you endow it with Fintype. Then, you use
docs#FiniteField.ringEquivOfCardEq to prove its equivalence to GaloisField p n (and thereby attain an embedding MyField ->+* GaloisField p n). then, by construction it suffices to make a map (ZMod p)[X] ->+* MyField, where you have an explicit generator of MyField available by construction.

[Adam Topaz]

Ok, sure. But you still need to write down the minimal polynomial of a generator, which we don’t yet have in mathlib as far as I know

[metakuntyyy]

Wait, can I prove the field property by hand. Like if I generate a structure with 0,1, a and b and define addition and multiplication on this structure and show that it is a field. Would that work?

import Mathlib


inductive Fieldfour : Type where
  | zero: Fieldfour
  | one: Fieldfour
  | a: Fieldfour
  | b: Fieldfour

def fieldfour.add : (@& Fieldfour) → (@& Fieldfour) → Fieldfour
  | Fieldfour.zero, x => x
  | a, Fieldfour.zero => a
  | Fieldfour.one, Fieldfour.one => Fieldfour.zero
  | Fieldfour.a, Fieldfour.one => Fieldfour.b
  | Fieldfour.one, Fieldfour.a => Fieldfour.b
  | Fieldfour.b, Fieldfour.one => Fieldfour.a
  | Fieldfour.one, Fieldfour.b => Fieldfour.a
  | Fieldfour.a, Fieldfour.a => Fieldfour.zero
  | Fieldfour.a, Fieldfour.b => Fieldfour.one
  | Fieldfour.b, Fieldfour.a => Fieldfour.one
  | Fieldfour.b, Fieldfour.b => Fieldfour.zero

def fieldfour.mul : (@& Fieldfour) → (@& Fieldfour) → Fieldfour
  | Fieldfour.zero, _ => Fieldfour.zero
  | _, Fieldfour.zero => Fieldfour.zero
  | Fieldfour.one, x => x
  | x, Fieldfour.one => x
  | Fieldfour.a, Fieldfour.a => Fieldfour.b
  | Fieldfour.a, Fieldfour.b => Fieldfour.one
  | Fieldfour.b, Fieldfour.a => Fieldfour.one
  | Fieldfour.b, Fieldfour.b => Fieldfour.a

That would manually create a structure with addition and multiplication. Is it easy to show that this is a field?

[Damiano Testa]

It is probably tedious, but it should not be hard.

[Damiano Testa]

If you add deriving DecidableEq to your type, most proofs will be by intros; cases <;> cases;...<;> decide.

[Edward van de Meent]

it might be simpler to prove some things if you base your type off of already existing structure, for example i used this definition in my (bachelors) thesis:

import Mathlib.Data.ZMod.Defs
import Mathlib.Tactic.FinCases

@[ext]
structure F4 where
  x0 : ZMod 2
  x1 : ZMod 2
deriving DecidableEq

instance : Fintype F4 := Fintype.ofList [⟨0,0⟩,⟨1,1⟩,⟨0,1⟩,⟨1,0⟩] (by
  intro ⟨a,b⟩
  fin_cases a <;> fin_cases b
  all_goals simp)

instance : Zero F4 := ⟨0,0⟩

instance : Add F4 := ⟨fun a b ↦ ⟨a.x0 + b.x0,a.x1 + b.x1⟩⟩

instance : Neg F4 := ⟨fun a ↦ a⟩ -- elements are mod 2, and -1=1, so it's id.

instance : One F4 := ⟨1,1⟩

-- multiplication such that both ⟨1,0⟩ and ⟨0,1⟩ are generators, and inverse is given by swapping fields.
instance : Mul F4 := ⟨fun a b ↦
  ⟨(a.x0 * b.x0) + (a.x0 + a.x1) * (b.x0 + b.x1),
  (a.x1 * b.x1) + (a.x0 + a.x1) * (b.x0 + b.x1)⟩
⟩
instance : Inv F4 := ⟨fun a ↦ ⟨a.x1,a.x0⟩⟩

[Edward van de Meent]

you can find the precise code i used there at this branch of mathlib

[Edward van de Meent]

although i do imagine quite some of these lemmas can be simplified

[Kevin Buzzard]

If I had to make F4 I'd surely define it as the quotient $\Z/2[X]/(X^2+X+1)$.