What is the form of a PrimalityProving`PrimeQCertificate?

Question

I understand the format of a proof of compositeness of an integer produced by PrimeQCertificate: it's well-documented that PrimeQCertificate[a] outputs one of:

• a triple {a, n-1, n} such that $a^{n-1} \not \equiv 1 \pmod{n}$ (that is, Fermat's test proves compositeness), or
• a triple {a, 2, n} such that $a^2 \equiv 1 \pmod n$ and $a \not \equiv \pm 1 \pmod{n}$ (which is a test derived from considering a difference of two squares).

For primality rather than compositeness, the documentation says it "uses the Pratt certificate and the Atkin-Morain certificate for primality."

What do these look like?

Answer 1

The Pratt test of n produces either the integer $2$, or a tuple {n, a, {certs}} where each cert is another certificate of primality, and such that

• $(a, n) = 1$
• $a^{n-1} \equiv 1 \pmod{n}$
• certs is a list of certificates for the primality of each prime $q \mid n-1$
• $a^{(n-1)/q} \not \equiv 1 \pmod{n}$ for all $q \mid n-1$

These conditions together force $n$ to satisfy the Lucas test for primality.

I have never seen an Atkin-Morain certificate generated.