AKS

[tirix]

A blueprint for formalizing Andrew Putman's AKS paper.

[tirix]

This is still in progress - we should detail how to prove aks61, and detail which theorems about the Galois limit fields are missing.
However I think we can still formalize the statement of Theorem 6.1.

[metakunt]

We also need this one.

To prove this bound we will also need a result about concave functions.
The following suffices.
Let $X= [a,b)$ be a half open interval and let $f: X \to \mathbb{R}$ and two times continously differentiable on $(a,b)$ such that $f^{\prime\prime} \leq 0$ for $x \in (a,b)$ then the following inequality holds for all $x\in X$

$$f(x) \leq f(a)+(x-a) f^{\prime}(a)$$

The estimate follows by https://www.wolframalpha.com/input?i=derivative+of+lb%28x%29%5E%287%2F2%29+at+x%3D+10000 which shows that $f^{\prime}(10000) < 1$ and
the second derivative is less than 0 for $x > e^{\frac{5}{2}}$, see https://www.wolframalpha.com/input?i=second+derivative+of+lb%28x%29%5E%287%2F2%29 and $f(10000)<10000$ by
https://www.wolframalpha.com/input?i=lb%2810000%29%5E%287%2F2%29

[metakunt]

I have already started proving some logarithm inequalities.
https://us.metamath.org/mpeuni/3lexlogpow5ineq3.html

[metakunt]

Note that the original paper does not use the algebraic closure, but instead computes everything in the polynomial ring mod $X^r-1,p$. Maybe we just need that result? But my field theory is not good at all to understand those arguments in detail. I don't even know what an element of the closure looks like and how you can compute addition and multiplication.

Here is the original paper: https://www.cse.iitk.ac.in/users/manindra/algebra/primality_v6.pdf

[metakunt]

I'd propose to add any theorem about Galois theory as an axiom until we know the minimal set needed. Then replace the axioms with theorems once we have found a sufficiently small set of results needed. This allows us to discard of extra hypotheses stating facts about Galois theory.

[metakunt]

I think the following is true.
Let $x\in \overline{\mathbb{F}}_p$, then there exists an $n\in \mathbb{N}$ such that $x\in \mathbb{F}_p^n$, indeed it holds that $\overline{\mathbb{F}}_p = \bigcup F_p^{n}$ where the union is over $n\in \mathbb{N}$
I think we have to construct the splitting field given the polynomial $X^{n!}-X$, but I have no idea...

[tirix]

it holds that $\overline{\mathbb{F}}_p = \bigcup F_p^{n}$ where the union is over $n\in \mathbb{N}$

I'm sorry I'm not an expert either here, but my understanding is that while you can informally think about the direct limit as a union, it's not an actual union. See the definition here, some of the elements will be conflated in the same equivalence class.

Note that the original paper does not use the algebraic closure, but instead computes everything in the polynomial ring mod. Maybe we just need that result?

Yes, in that sense the original paper is more elementary, and the mathematical tools will be more readily available in set.mm. On the other hand the objects used in Andrew Putman's paper, such as the limit Galois fields, are very interesting and it would be very nice to progress in their formalization.

I'd propose to add any theorem about Galois theory as an axiom until we know the minimal set needed. Then replace the axioms with theorems once we have found a sufficiently small set of results needed. This allows us to discard of extra hypotheses stating facts about Galois theory.

Yes we can do that. We'll still need to identify and correctly formalize the different theorems needed.

[tirix]

FYI here is the current view of the dependencies:

Maybe I should find a way for in-progress PR to be browsable too.

[metakunt]

Lemma 4.1 seems doable/easier to state. I will commit a draft once I find a bit of time. I'll try to break it into small steps so that the bigger picture seems apparent.

Edit: Damn, that's a good picture. It will get even bigger.

[metakunt]

Ok I have tried to formalize the hypotheses for a part of the claim 3.
It goes as follows, $E$ is a subset of the integers and $f$ is the homomorphism that maps the integers to $\mathbb{Z}/r\mathbb{Z}$
We need to show that $f(E)=\mathbb{Z}/r\mathbb{Z}$ we are using several facts, namely that the integer powers are in $E$. Since $gcd(n,r)=1$ we know that n is the generator of the multiplicative group $(\mathbb{Z}/r\mathbb{Z}^{\ast})$
We have shown that the powers of n generate under this map the whole group and the elements of the group can't be more than the order we can combine the inequalities transitively to show the claim.

This lemma seems the most malleable, it is small, it contains lots of informations and it would not only be a good result to formalize but it would also give us insight how to move forward.

[tirix]

I think you can write this set as:

E = ran ( k e. NN0 , j e. NN0 |-> ( ( ( N / P ) ^ k ) x. ( P ^ j ) ) ) )

[metakunt]

Ah nevermind, I didn't see that p divides N, yeah, that works. I assumed that N was arbitrary, then $\frac{N}{p}$ could be in $\mathbb{Q}-\mathbb{Z}$ justifying my version. Since I missed that it is clear that $\frac{N}{p}$ is an integer. I will fix the description.

[metakunt]

Also I think we should tackle this claim first. It is small and it should be straightforward to prove.

[tirix]

I think I should already merge this so it appears on the blueprints page, what do you think?

[metakunt]

Ah I think the author did a grave mistake in his paper. He claims that for all $a\geq 1$

$$2^{a+1}< \binom{2a+1}{a}$$

But this is clearly wrong for a=1 since

$$2^{a+1}=2^2=4<3=\binom{3}{1}=\binom{2\cdot1+1}{1}=\binom{2a+1}{a}$$

is obviously false. And his proof in the footnote seems also wrong. I think that the theorem is true for $a\geq 2$ and that might be enough.

Since it appears that this is the only step where $a\geq 2 $ is needed we might have to update the restriction to $a\geq 4$.

Either he did a mistake or I've missed something.

What do you think?

[metakunt]

Yeah, good idea. Before you merge I would be happy if you could quickly review my last comment, so that it doesn't get lost.

[metakunt]

Checking this one the original authors were a little bit more careful in Lemma 4.9
https://www.cse.iitk.ac.in/users/manindra/algebra/primality_v6.pdf
They see that the inequality only holds if $a\geq 2 $
However we would still need a proof of $2 \leq \lfloor \sqrt{t\cdot \log_2^2 n} \rfloor$

By those equations alone it suffices if $4\leq t$ however I don't see that one yet.

[tirix]

What do you think?

Obviously you're right!