Working draft as of June 18, 2003

• Please do not cite without permission
• Comments welcome

QUADRATIC RECIPROCITY IN ISABELLE

David Emmanuel Gray

Carnegie Mellon University

1. A Brief History of the Genesis of Quadratic Reciprocity

The history of quadratic reciprocity begins in the third century A.D. with Diophantos’ Arithmetica, with the claim that a = x² + y² had no solution in integers, when a was of the form 4n + 3. In our editions of Diophantos’ work, there is no proof of this statement provided. Nevertheless, Pythagorean methods – known to him – suggest an easy proof [1]. Of particular interest to later thinkers would be how this applied to more general problems concerning prime numbers.

In the late seventeenth century, Fermat carefully studied the surviving editions of Diophantos’ work, and he became intrigued by how it might allow one to derive properties of the forms of prime numbers. In a letter to his friend Mersenne, he stated that a prime p is of the form 4n + 1 iff p = x² + y² for some integers x and y. While he provided no proof for this, he claimed it could be done using his method of infinite descent [1]. This led Fermat to other questions concerning different forms of prime numbers. While studying primes of the form 2ⁿ + 1 for positive integers n, Fermat proposed his “little theorem”: if p is prime, x an integer, and x is not divisible by p, then p divides x^{p – 1} – 1. Over a hundred years later, Euler would finally confirm both of Fermat’s statements [2].

In studying – and proving much of – Fermat’s work on primes, Euler himself became interested in the more general questions concerning primes of the form x² + ay², where a was a positive integer not divisible by p. Independently of Euler, Legendre became interested in this type of question as well. In order to answer it, they both became particularly interested in what are now called the quadratic residues of prime numbers. That is, if p is prime and a an integer, we say that a is a quadratic residue modulo p if there is some x such that p divides x² – a. In order to represent this property, Legendre introduced the symbol, (a / p), now called the Legendre symbol [2]. It is defined as

While studying quadratic residues, Euler discovered that they yielded a strong necessary condition for a prime to be of the form x² + ay². That is, if p = x² + ay², where p does not divide a, then (-a / p) = 1. This implies that a prime is of the form x² – ay², p not dividing a, then a is a quadratic residue modulo p. Such concerns lead Euler to refine Fermat’s Little Theorem by proving a “criterion” that if p is an odd prime, a an integer, and p does not divide a, then p divides a^{(p – 1) / 2} – (a / p). (Note that Euler did not know of the Legendre symbol, but using it makes his results more compactly stated.)

When deriving properties for his operation, Legendre became interested in the case of primes p of the form x² ± qy², where q was a prime distinct from p. Interestingly, he found that he could not just consider (q / p); he had to also deal with (p / q) [2]. This led him to conjecture that (p / q) depended on (q / p) in the following manner:

This was an initial formulation of what is now known as Gauss’ Law of Quadratic Reciprocity, which states that for distinct odd primes p and q, that

Quadratic reciprocity is a deep and important result in number theory. It allows one to evaluate the Legendre Symbol easily for large prime numbers, especially when compared to an alternative like Euler’s Criterion. Even more importantly, though, it is essential in helping solve that general problem of characterizing the forms of prime numbers when (a / p) = 1. For instance, it allows one to easily prove that there are infinitely many primes of the form 10k + 1. (See [3] for a proof.)

Unknown to Legendre, Euler also formulated this property. Thus, in their studies, both figures were invariably drawn towards it. However, neither one of them was able to prove it.

The first proof of this property would come almost two decades later in Gauss’ Disquisitiones. In order to do it – and make things clearer – Gauss first introduced the notion of congruences. If a, b, and m are integers, and m divides a – b, then a is congruent to b modulo m. This is written as a º b (mod m). Thus Fermat’s Little Theorem is formulated as: if p is prime, x an integer, and x is not divisible by p, then

x^{p – 1} º 1 (mod p)

Similarly, Euler’s Criterion becomes: if p is an odd prime, a an integer, and p does not divide a, then

Also, we can say that a is a quadratic residue modulo p if there is some x such that x² º a (mod p). This notion of congruences not only makes expressing these important properties easier, but it has become a central notion in number theory for its own right [2].

In describing the process of proving quadratic reciprocity, Gauss said that “for a whole year this theorem tormented me and absorbed my greatest efforts until at last I obtained a proof” [4]. Nevertheless, Gauss did not stop there. By the end of his lifetime he furnished no less than eight different proofs of this property. He claimed that while his earlier proofs “leave nothing to be desired as regards rigor, they are derived from sources much too remote” [4]. In nearly every proof, Gauss pioneered new methods and techniques in order to find the most “natural” proof. Furthermore, these new methods would open up significant uncharted areas in number theory. Nevertheless, in the end, it appears that Gauss was never fully satisfied with any of his proofs [3].

To date, there are over one hundred fifty published proofs of quadratic reciprocity. Yuri Manin notes that the idea is not to come up with more convincing arguments for quadratic reciprocity because “one proof is sufficiently convincing. The point is, that proving is the way we are discovering new territories, new features of the mathematical landscape” [5].

In this spirit, we have formalized quadratic reciprocity in the semi-automated theorem prover Isabelle. Previously, David M. Russinoff formalized quadratic reciprocity in the Boyer-Moore theorem prover to generate a proof mechanically [3]. In his proof, Russinoff follows a method for proving quadratic reciprocity that is attributed to Eisenstein. This proof makes use of both Fermat’s Little Theorem and Euler’s Criterion, along with Wilson’s Theorem and Guass’ Theorem. Our proof shall follow this same path.

In this paper, I shall present aspects of our fully formalized proof in Isabelle. In order to do this, the functionality and syntax of Isabelle will be outlined. Then I shall provide a detailed guide to the important lemmas that we formalized in Isabelle. I conclude with some remarks about this proof in general.

2. Higher-Order Logic in Isabelle

Isabelle [6] is a generic theorem proving environment for implementing logical formalisms. It has been instantiated to support reasoning in several logics, including first-order logic and higher-order logic. Isabelle also provides several generic tools, such as simplifiers and classical theorem provers, which can be applied to these logics. Of particular interest is Isabelle/HOL, the specialization of Isabelle for Higher-Order Logic (HOL). Isabelle is implemented in the functional programming language ML, making Isabelle/HOL a typed logic whose type system resembles that of ML. Furthermore this “functional” aspect is reflected in the concrete syntax of Isabelle/HOL through the implementation of types, terms, formulae, and variables [7].

2.1 Types

In Isabelle/HOL, there are several different classes of types available, along with many libraries of pre-defined instantiations of these types. Of these classes, three are of particular interest:

• Base Types – These are the basic types. In our proof the most commonly used are
• bool, the type of truth values,
• int, the type of integers, and
• nat, the type of natural numbers.
• Constructed Types – These are types that are “constructed” in that they require additional type(s) as a parameter(s). The one used in our proof is
• set, the type of sets. In Isabelle, the notion x : A is a formula (see 2.2 below) that asserts x is an element of the set A. The commonly used instantiations of this type will be
• zprime, of type int set, which is the set of all prime integers, and
• zEven and zOdd, of types int set, which are the sets of all even and odd integers respectively.
• Function Types – These types are denoted by =>. For instance, an identity function for integers would have type int => int. The commonly used functions in our proof are
• The standard binary arithmetic operations, + (addition), - (subtraction), * (multiplication), div (quotient), mod (remainder/modulo), which are supported for int’s and nat’s,
• The additional operations of ^ (exponentiation for int’s and nat’s though the exponent is a nat for both) and zfact (factorial for int’s),
• The standard set operations, Un (union), Int (intersection), <*> (product), and card (cardinality) for set’s,
• The additional operations of image (encoded as f ` A, which is the image of the function f applied to domain A), setsum (set summation – encoded as setsum f A, which returns f(a₁) + f(a₂) + … + f(a_n), where a_i Î A), and gsetprod (set product, similar to setsum, but with multiplication),
• The relations < (less than for int’s and nat’s, proper-subset for set’s), <= (less than or equal for int’s and nat’s, subset for set’s), dvd (divides for int’s and nat’s), zcong (congruence for int’s), and finite (finite for set’s), which, as expected of relations, return bool values, and
• The conversion operations int and nat, which convert between the types of int and nat.

2.2 Terms and Formulae

As is similar in functional programming, applying functions to arguments forms terms in Isabelle. Given a function f of type t₁ Þ t₂ and a term t of type t₁ then f t will be a term of type t₂. Terms may also be lambda (l)-abstractions, similar to terms in the l-calculus. Such abstractions will be made use of in our proof. For instance, in Isabelle, lx. x (the identity function) would be represented as (%x. x).

Logical formulae are represented as terms of type bool. Also there are the basic constants True and False along with the standard logical connectives: ~ (not), & (and), |(or), and --> (implication). Equality is also available in the form of the infix function = that can be applied to pairs of any type. Quantifiers are written as EX x. P for the existential and ALL x. P for the universal.

Finally, in order to disambiguate the types of terms, it is often necessary to present terms using type constraints with the syntax ::. This is especially necessary when overloaded operators – that is, operators defined for many different types – such as *, + and < are used. For instance, x < y, does not specify the types of x and y, while x < (y :: int) specifies that there are both int’s.

2.3 Variables

Isabelle distinguishes between three different types of variables when proving. These three are:

• Free Variables – As expected, those variables not bounded by quantifiers,
• Bound Variables – Those variables bounded by quantifiers, automatically renamed in order to avoid conflicts with free variables, and
• Schematic (Unknown) Variables – Logically, these variables are free variables. In fact, Isabelle automatically converts all free variables in a lemma or theorem into these, representing them with a ? as their first character. These variables may be instantiated by other terms during the proof process, unlike the ordinary variables that must remain fixed. Furthermore, Isabelle will automatically instantiate unknowns suitably when the lemma or theorem is used in some other proof.

2.4 Lemmas and Theorems

In Isabelle, propositions are expressed as lemmas and theorems, represented in the form [| T₁, T₂, … T_n |] ==> C, where the T_i’s are the hypotheses and C is the conclusion. All are formulas. Propositions without hypotheses are expressed merely as C. More specific information regarding how types, terms, and variables are handled in Isabelle can be found in an online tutorial [7], while the instantiation of the various specific types, functions, and relations in Isabelle/HOL can be found in the Isabelle/HOL library [8], as well as its number theory library [9]. Consult the tutorial as well for the mechanisms for proving propositions.

3. The Proof

In our proof of quadratic reciprocity, we followed the route previously blazed by Russinff in his automated proof. There he formalized Eisenstein’s proof of quadratic reciprocity, using a transformation of Euler’s Criterion called Gauss’ Lemma [3]. This lemma leads to a relatively simple, but very interesting, geometric proof of quadratic reciprocity.

In order to formalize this, our proof makes use of several existing libraries in Isabelle/HOL geared towards number theory [9]. In particular, we use Rasmussen’s library of properties for prime integers, greatest common divisor, and congruence [10]. In addition to these libraries, our proof of quadratic reciprocity required that we develop new libraries of properties for finite sets [11], the divides relation, congruence [12], residues [13], and even and odd integers [14].

We also use Rasmussen’s proofs of Fermat’s Little Theorem [15] and Wilson’s Theorem [16] in order to prove Euler’s Criterion [17]. This is turn is used to prove Gauss’ Lemma [18]. Finally this sets us up a geometric interpretation which leads to the proof of Quadratic Reciprocity [19].

3.1 Fermat’s Little Theorem, Wilson’s Theorem, and Residues

In Isabelle, the zcong relation represents congruence. So a º b (mod m) is encoded as zcong a b m. However, Isabelle supports a more natural representation of zcong a b m as [a = b] mod (m). As stated above, Fermat’s Theorem states that for any prime p and x, with x not divisible by p,

x^{p – 1} º 1 (mod p)

This is encoded in Isabelle as

THEOREM 3.1.1 (Fermat’s Little Theorem [15])

[| p : zprime; ¬ p dvd x |] ==> [x ^ nat (p - 1) = 1] (mod p)

Similarly Wilson’s Theorem, which states that for any prime p,

(p – 1)! º -1 (mod p)

appears in Isabelle as

THEOREM 3.1.2 (Wilson’s Theorem [16])

p : zprime ==> [zfact (p - 1) = -1] (mod p)

These two theorems will prove useful when proving Euler’s Criterion (see 3.2 below).

We then formalize the definition of whether there is a quadratic residue modulo m for x as

DEFINITION 3.1.4 (Quadratic Residue)

QuadRes m x == EX y. ([(y ^ 2) = x] (mod m))

Finally, the Legendre Symbol, which, as noted before, is defined as

is accordingly formalized as the following operation:

DEFINITION 3.1.5 (The Legendre Operation)

Legendre a p == (if ([a = 0] (mod p)) then 0

else if (QuadRes p a) then 1

else -1)

Note that a º 0 (mod p) is equivalent to a divides p.

These definitions, along with other related definitions and the proofs of simple properties and relationships, are found in [13].

3.2 Euler’s Criterion

As noted above, Euler’s Criterion plays an important part in proving quadratic reciprocity. Recall that it states that for any odd prime p

The proof of this criterion consists of three parts: it must hold that

(1) if (a / p) = 0,

(2) if (a / p) = 1, and

(3) if (a / p) = -1.

The proofs of the (1) and (2) are trivial, while (3) more difficult.

The informal proof behind the formalization of (1) is that if (a / p) = 0, then a º 0 (mod p). Therefore,

a^{(p – 1) / 2} º 0^{(p – 1) / 2} (mod p)

º 0 (mod p)

This gives us the following lemma in Isabelle:

LEMMA 3.2.1

[| 2 < p; p : zprime; [a = 0] (mod p) |] ==>

[0 = a ^ nat ((p - 1) div 2)] (mod p)

Note that saying 2 < p is equivalent to saying that p is odd (in fact, there is a lemma to that effect in [14]).

The proof for (2) argues that if (a / p) = 1, then we can say a T 0 (mod p) and that, for some n, a º n² (mod p). And so

a^{(p – 1) / 2} º (n²)^{(p – 1) / 2} (mod p)

º n^{p – 1} (mod p)

And from Fermat’s Little Theorem, we then have a^{(p – 1) / 2} º 1 (mod p). This gives us

LEMMA 3.2.2

[| 2 < p; p : zprime; ¬ [a = 0] (mod p); QuadRes p a |] ==>

[a ^ nat ((p - 1) div 2) = 1] (mod p)

Proving (3) is not as simple. If (a / p) = -1, then we know that a T 0 (mod p) and that a is not a quadratic residue modulo p. We then can partition the set {1, 2, …, p - 1} into pairs (j, j^-1), where j^-1 º j^p-2a (mod p), such that j j^-1 º a (mod p). Since a is not a quadratic residue then j and j^-1 must be distinct, and so there are (p – 1) / 2 pairs. Taking the product of the union of these partitions shows that (p – 1)! º a^{(p – 1) / 2} (mod p). Finally, by Wilson’s Theorem, a^{(p – 1) / 2} º -1 (mod p).

The majority of the work formalizing Euler’s Criterion involved the representing and handing the (j, j^-1) pairs, along with using various properties of finite sets. The result is

LEMMA 3.2.3

[| 2 < p; p : zprime; ¬ [x = 0] (mod p); ¬ QuadRes p x |] ==>

[x ^ nat ((p - 1) div 2) = -1] (mod p)

From these, Euler’s Criterion is formalized as

THEOREM 3.2.4 (Euler’s Criterion)

[| 2 < p; p : zprime |] ==>

[Legendre a p = a ^ nat ((p - 1) div 2)] (mod p)

The entire formalized proof of this theorem can be found in [17].

3.3 Gauss’ Lemma

In our proof of quadratic reciprocity, we derive Gauss’ Lemma from Euler’s Criterion, which states that for any odd prime p consider the set B = {a, 2a, 3a, …, {(p – 1) / 2}a}, where a T 0 (mod p). If E is the set of the least positive residues modulo p of the elements of B which are greater than p / 2, then

In formalizing a poof of this lemma, we roughly followed the presentation of Gauss’ Lemma given by Ivan Niven and Herbert Zuckerman [20]. We first began by defining some initial sets:

DEFINITION 3.3.1 (A := {1, 2, …, (p – 1) / 2})

A == {(x::int). 0 < x & x <= ((p - 1) div 2)}

DEFINITION 3.3.2 (B := {1a, 2a, …, {(p – 1) / 2}a})

B == (%x. x * a) ` A

We immediately note

LEMMA 3.3.3 (|A| = (p – 1) / 2)

card A = nat ((p - 1) div 2)

LEMMA 3.3.4 (|A| = |B|)

card B = card A

We then define the set of residues modulo p as

DEFINITION 3.3.5 (C := {{1a mod p, 2a mod p, …, {(p – 1) / 2}a mod p})

C == (StandardRes p) ` B

We have defined StandardRes as a renaming of the mod function, but with arguments reversed, so StandardRes p a is equivalent to a mod p. Now we have

LEMMA 3.3.6 (|C| = |B|)

card C = card B

We then partition C into two sets D and E, defined by

DEFINITION 3.3.7 (D := {x Î C | x <= (p – 1) / 2})

D == C Int {x. x <= ((p - 1) div 2)}

DEFINITION 3.3.8 (E := {x Î C | (p – 1) / 2 < x})

E == C Int {x. ((p - 1) div 2) < x}

E is the set of all residues that exceed (p – 1) / 2, and D is the set of the remaining residues. And so we have

LEMMA 3.3.9 (|C| = |D| + |E|)

card C = card D + card E

Now consider the set F, defined as

DEFINITION 3.3.10

F == (%x. (p - x)) ` E

That is, if E := {r₁, r₂, …, r_n}, then F := {p – r₁, p – r₂, … p – r_n}. We then have

LEMMA 3.3.11 (|F| = |E|)

card F = card E

Now no element of F is an element of D, and so

LEMMA 3.3.12 (F È D = Æ)

F Int D = {}

Where {} is the empty set. Therefore |D U F| = |D| + |F|. From the ongoing, we see that

(p – 1) / 2 = |A|

= |B|

= |C|

= |D| + |E|

= |D| + |F|

And so we derive

LEMMA 3.3.13 (|F Ç D| = (p – 1) / 2)

card (F Un D) = nat ((p - 1) div 2)

And so |D U F| = |A|. Furthermore, since D Í A and F Í A, we have

LEMMA 3.3.14 (F Ç D Í A)

(F Un D) <= A

Now we can derive

LEMMA 3.3.15 (F Ç D = A)

F Un D = A

And from LEMMA 3.3.12 we know (PD)(PF) = P(D U F). Thus we have

LEMMA 3.3.16 ((PD)(PF) = PA)

(gsetprod id D) * (gsetprod id F) = gsetprod id A

Note that id is just the identity function (id x = x). Now we get

PF º P_jÎE (p – j) (mod p)

º P_jÎE ((p – j) mod p) (mod p)

º P_jÎE (-j) (mod p)

º (PE)(-1)^|E| (mod p)

This is formalized in

LEMMA 3.3.17 (PF º (PE)(-1)^|E| (mod p))

[gsetprod id F = ((-1) ^ (card E)) * (gsetprod id E)] (mod p)

Putting all the above together we have

PA º (