• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • Arithmetic
      • Lispfloat
      • Arithmetic-1
      • Number-theory
      • Proof-by-arith
      • Arith-equivs
      • Number-theory
        • Euler
        • Euclid
        • Fermat
      • Arithmetic-3
      • Arithmetic-2
      • Arithmetic-light
      • Arithmetic-5
    • Bit-vectors
    • Algebra

• Number-theory

Euler

This book contains a proof of Euler's Criterion for quadratic residues

This book contains a proof of Euler's Criterion for quadratic residues: If p is an odd prime and m is not divisible by p, then

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

Along the way, we also prove Wilson's Theorem: If p is prime, then mod((p-1)!,p) = p-1. Finally, as a consequence of Euler's Criterion, we derive the First Supplement to the Law of Quadratic Reciprocity: -1 is a quadratic residue mod p iff mod(p,4) = 1. The proof depends on Fermat's Theorem:

Definitions and Theorems

Let p be a prime, let m be relatively prime to p, and let 0 < j < p. Then there exists a unique j' such that 0 < j' < p and

mod(j*j',p) = mod(m,p), 

called the associate of j w.r.t. a mod p.

Function: associate

(defun associate (j m p)
       (mod (* m (expt j (- p 2))) p))

Theorem: associate-property

(defthm associate-property
        (implies (and (primep p)
                      (integerp m)
                      (not (zp j))
                      (< j p)
                      (not (divides p m)))
                 (equal (mod (* (associate j m p) j) p)
                        (mod m p)))
        :rule-classes nil)

Theorem: associate-bnds

(defthm associate-bnds
        (implies (and (primep p)
                      (integerp m)
                      (not (zp j))
                      (< j p)
                      (not (divides p m)))
                 (and (not (zp (associate j m p)))
                      (< (associate j m p) p)))
        :rule-classes (:forward-chaining))

Theorem: associate-is-unique

(defthm associate-is-unique
        (implies (and (primep p)
                      (integerp m)
                      (not (zp j))
                      (< j p)
                      (not (divides p m))
                      (integerp x)
                      (equal (mod m p) (mod (* j x) p)))
                 (equal (associate j m p) (mod x p)))
        :rule-classes nil)

Theorem: associate-of-associate

(defthm associate-of-associate
        (implies (and (primep p)
                      (integerp m)
                      (not (zp j))
                      (< j p)
                      (not (divides p m)))
                 (equal (associate (associate j m p) m p)
                        (mod j p))))

Theorem: associate-equal

(defthm associate-equal
        (implies (and (primep p)
                      (integerp m)
                      (integerp j)
                      (not (divides p m))
                      (not (zp j))
                      (< j p)
                      (not (zp i))
                      (< i p))
                 (equal (equal (associate j m p)
                               (associate i m p))
                        (equal i j))))

Theorem: associate-square

(defthm associate-square
        (implies (and (primep p)
                      (integerp m)
                      (not (divides p m))
                      (not (zp j))
                      (< j p))
                 (iff (= (associate j m p) j)
                      (= (mod (* j j) p) (mod m p))))
        :rule-classes nil)

If there exists x such that mod(x*x,p) = mod(m,p), then m is said to be a (quadratic) residue mod p.If m is a residue mod p, then there are exactly 2 roots of mod(x*x,p) = mod(m,p) in the range 0 < x < p.

Function: root1

(defun root1 (m p)
       (find-root (1- p) m p))

Theorem: res-root1

(defthm res-root1
        (implies (and (primep p) (residue m p))
                 (and (not (zp (root1 m p)))
                      (< (root1 m p) p)
                      (equal (mod (* (root1 m p) (root1 m p)) p)
                             (mod m p))))
        :rule-classes nil)

Function: root2

(defun root2 (m p) (- p (root1 m p)))

Theorem: res-root2

(defthm res-root2
        (implies (and (primep p) (residue m p))
                 (and (not (zp (root2 m p)))
                      (< (root2 m p) p)
                      (equal (mod (* (root2 m p) (root2 m p)) p)
                             (mod m p))))
        :rule-classes nil)

Theorem: associate-roots

(defthm associate-roots
        (implies (and (primep p)
                      (integerp m)
                      (not (divides p m))
                      (residue m p))
                 (and (equal (associate (root1 m p) m p)
                             (root1 m p))
                      (equal (associate (root2 m p) m p)
                             (root2 m p))))
        :rule-classes nil)

Theorem: only-2-roots

(defthm only-2-roots
        (implies (and (primep p)
                      (integerp m)
                      (not (divides p m))
                      (residue m p)
                      (not (zp j))
                      (< j p)
                      (= (associate j m p) j))
                 (or (= j (root1 m p))
                     (= j (root2 m p))))
        :rule-classes nil)

Theorem: roots-distinct

(defthm roots-distinct
        (implies (and (primep p)
                      (not (= p 2))
                      (residue m p))
                 (not (= (root1 m p) (root2 m p))))
        :rule-classes nil)

For 0 <= n < p, we construct a list associates(n,m,p) of distinct integers between 1 and p-1 with the following properties:

• If 1 <= j <= n, then j is in associates(n,m,p).
• If j is in associates(n,m,p), then so is associate(j,m,p).

Function: associates

(defun associates (n m p)
       (if (zp n)
           (if (residue m p)
               (cons (root2 m p)
                     (cons (root1 m p) nil))
               nil)
           (if (member n (associates (1- n) m p))
               (associates (1- n) m p)
               (cons (associate n m p)
                     (cons n (associates (1- n) m p))))))

Theorem: member-associates

(defthm member-associates
        (implies (and (primep p)
                      (integerp m)
                      (not (divides p m))
                      (integerp n)
                      (< n p)
                      (not (zp j))
                      (< j p))
                 (iff (member (associate j m p)
                              (associates n m p))
                      (member j (associates n m p)))))

We shall show that associates(p-1,m,p) is a permutation of positives(p-1).

Theorem: subset-positives-associates

(defthm subset-positives-associates
        (subsetp (positives n)
                 (associates n m p)))

Theorem: member-self-associate

(defthm member-self-associate
        (implies (and (primep p)
                      (integerp m)
                      (not (divides p m))
                      (not (zp j))
                      (< j p)
                      (equal (associate j m p) j))
                 (member j (associates n m p))))

Theorem: distinct-positives-associates-lemma

(defthm distinct-positives-associates-lemma
        (implies (and (primep p)
                      (not (= p 2))
                      (integerp m)
                      (not (divides p m))
                      (integerp n)
                      (< n p))
                 (distinct-positives (associates n m p)
                                     (1- p)))
        :rule-classes nil)

Theorem: distinct-positives-associates

(defthm distinct-positives-associates
        (implies (and (primep p)
                      (not (= p 2))
                      (integerp m)
                      (not (divides p m)))
                 (distinct-positives (associates (1- p) m p)
                                     (1- p)))
        :rule-classes nil)

We shall require a variation of the pigeonhole principle.

Theorem: pigeonhole-principle-2

(defthm pigeonhole-principle-2
        (implies (and (natp n)
                      (distinct-positives l n)
                      (subsetp (positives n) l))
                 (perm (positives n) l))
        :rule-classes nil)

Theorem: perm-associates-positives

(defthm perm-associates-positives
        (implies (and (primep p)
                      (not (= p 2))
                      (integerp m)
                      (not (divides p m)))
                 (perm (positives (1- p))
                       (associates (1- p) m p)))
        :rule-classes nil)

It follows that the product of associates(p-1,m,p) is (p-1)! and its length is p-1.

Theorem: times-list-associates-fact

(defthm times-list-associates-fact
        (implies (and (primep p)
                      (not (= p 2))
                      (integerp m)
                      (not (divides p m)))
                 (equal (times-list (associates (1- p) m p))
                        (fact (1- p))))
        :rule-classes nil)

Theorem: perm-len

(defthm perm-len
        (implies (perm l1 l2)
                 (= (len l1) (len l2)))
        :rule-classes nil)

Theorem: len-positives

(defthm len-positives
        (equal (len (positives n)) (nfix n)))

Theorem: len-associates

(defthm len-associates
        (implies (and (primep p)
                      (not (= p 2))
                      (integerp m)
                      (not (divides p m)))
                 (equal (len (associates (+ -1 p) m p))
                        (1- p))))

Theorem: len-associates-even

(defthm len-associates-even
        (implies (and (primep p)
                      (not (= p 2))
                      (integerp m)
                      (not (divides p m))
                      (integerp n)
                      (< n p))
                 (integerp (* 1/2 (len (associates n m p)))))
        :rule-classes (:type-prescription))

On the other hand, we can compute the product of associates(p-1,a,p) as follows.

Theorem: times-list-associates

(defthm
    times-list-associates
    (implies
         (and (primep p)
              (not (= p 2))
              (integerp m)
              (not (divides p m))
              (< n p))
         (equal (mod (times-list (associates n m p)) p)
                (if (residue m p)
                    (mod (- (expt m (/ (len (associates n m p)) 2)))
                         p)
                    (mod (expt m (/ (len (associates n m p)) 2))
                         p))))
    :rule-classes nil)

Both Wilson's Theorem and Euler's Criterion now follow easily.

Theorem: euler-lemma

(defthm euler-lemma
        (implies (and (primep p)
                      (not (= p 2))
                      (integerp m)
                      (not (divides p m)))
                 (equal (mod (fact (1- p)) p)
                        (if (residue m p)
                            (mod (- (expt m (/ (1- p) 2))) p)
                            (mod (expt m (/ (1- p) 2)) p))))
        :rule-classes nil)

Theorem: wilson

(defthm wilson
        (implies (primep p)
                 (equal (mod (fact (1- p)) p) (1- p)))
        :rule-classes nil)

Theorem: euler-criterion

(defthm euler-criterion
        (implies (and (primep p)
                      (not (= p 2))
                      (integerp m)
                      (not (divides p m)))
                 (equal (mod (expt m (/ (1- p) 2)) p)
                        (if (residue m p) 1 (1- p))))
        :rule-classes nil)

The First Supplement is the case a = 1

Theorem: first-supplement

(defthm first-supplement
        (implies (and (primep p) (not (= p 2)))
                 (iff (residue -1 p) (= (mod p 4) 1)))
        :rule-classes nil)