------------------------------------------------------------------------------------
David M. Russinoff, March 2007
Last modified May 21, 2007
------------------------------------------------------------------------------------

This directory contains an ACL2 proof script for the law of quadratic reciprocity:

  if p and q are distinct odd primes, then 
    (p is a quadratic residue mod q <=> q is a quadratic residue mod p)
     <=>
    ((p-1)/2) * ((q-1)/2) is even.

The proof is an adaptation of the author's Nqthm formalization of the same theorem:

http://www.cs.utexas.edu/users/boyer/ftp/nqthm/nqthm-1992/examples/basic/new-gauss.events

The proof may be certified by loading the file certify.lsp:

  ACL2 !>(ld "certify.lsp")

The script consists of six ACL2 books:

  "euclid"
     Divisibility, primes, and two theorems of Euclid: 
     (1) The infinitude of the set of primes
     (2) if p is a prime and p divides a * b, then p divides either a or b.

  "fermat"
     Fermat's Theorem: if p is a prime and p does not divide m, then 
     mod(m^(p-1),p) = 1.

  "euler"
     Quadratic residues and Euler's Criterion: if p is an odd prime and p does
     not divide m, then

          mod(m^((p-1)/2),p) = 1 if m is a quadratic residue mod p
                               p-1 if not.

     A by-product of the proof is Wilson's Theorem: mod((p-1)!,p) = p-1.
     As a consequence, we also prove the First Supplement to the Law of Quadratic
     Reciprocity: -1 is a quadratic residue mod p iff mod(p,4) = 1.

  "gauss"
      Gauss's Lemma:  Let p be an odd prime and let m be relatively prime to p.
      Let mu be the number of elements of the sequence

        (mod(m,p), mod(2*m,p), ..., mod(((p-1)/2)*m,p))

      that exceed (p-1)/2.  Then m is a quadratic residue mod p iff mu is even.
      As a corollary, we also prove the Second Supplement to the Law of Quadratic
      Reciprocity: 2 is a quadratic residue mod p iff mod(p,8) is either 1 or -1.

  "eisenstein"
      A formalization of Eisenstein's proof of quadratic reciprocity.

  "mersenne"
      An application to the Mersenne prime problem by way of a theorem of Euler:
      if p and 2*p+1 are both prime and mod(p,4) = 3, then 2^p-1 is divisible by
      2*p+1.