Interface 5: primality is a verifier subroutine

Agrawal–Kayal–Saxena gives deterministic polynomial-time primality testing AKS,AKSErratum. The source's appendix presents its own polynomial-congruence primality argument SourcePrimality. These are distinct proof objects.

For the local finite circuit, neither general primality algorithm is needed: all primes which occur are at most $13$, and their primality is checked directly below. Consequently, the finite certificate does not import or verify the source appendix.