After more than a month of working with Aristotle of Harmonic, I’m reasonably confident that we’ve shown either in Lean or in Pari/gp enough to justify the statement:
Let q<57000 be an odd prime such that 4q=a^2+27 for some positive integer a. Let N be an odd prime such that N=/=q and gcd(a,N)=1. Let s1 == (-a-3)/6 (mod q) and s2 == (a-3)/6 (mod q). Let f=x^3-qx-q. Assume that f is irreducible modulo N. Let c == N^((q-1)/3) (mod q). Let K be a splitting field of f over F_N. Let alpha be a root of f in K. Let beta in K be such that
2a beta = 6 alpha^2 – (a+9)alpha – 4q and gamma in K be such that alpha + beta + gamma = 0.
Then, alpha^N = gamma if c == s1 (mod q) and
alpha^N = beta if c == s2 (mod q).
The Lean proofs for general q are in the following four files:
1- 11e5bcda-f90d-44d0-93f2-10b7e059f17d-output.lean (Main Theorem in the cyclotomic setting)
2- 4daadaec-7f20-4766-8f19-9997b90ad30f-output.lean (Differences of Gaussian Periods are independent of generator of (Z/qZ)*)
3- c44fa606-0342-4dc8-81ec-6962d6e5a885-output.lean (Main Theorem in the setting where K is a splitting field of f over F_N)
4- d4a059c4-fe50-4ea3-97e7-b6c52b31ad13-output.lean (If c != 1 (mod q), then f is irreducible over F_N)
These are available on Github here: https://github.com/mariotrevi/frob-orientation-lean.
The limitation: q<57000 is attributable to two algebraic verifications that have to be done for each q. One is that the differences of Gaussian periods are roots of X^3 – qX – q. The second is verifying that 2a beta = 6 alpha^2 – (a+9)alpha – 4q. In the cyclotomic setting, each of alpha, beta, and gamma are defined as differences of Gaussian periods.
