The Foursquare Theorem
This is about Lagrange’s four-square theorem, which states that every natural number can be expressed as the sum of four squares. For example,
The proof given on the Wikipedia page is only an existence proof, but I was able to find a mostly constructive proof elsewhere online. I want to present an outline of the proof along with some code that carries out the construction. Here’s a preview:
*Main> foursquare 123456789 (-2142,8673,6264,-2100)
Outline of the constructive proof
To write a number as the sum of four squares:
If is composite, find its prime factors and write each of the factors as the sum of four squares. Then combine them pairwise using Euler’s four-square identity, which shows that the product of two numbers that are the sum of four squares can itself be written as the sum of four squares.
For each prime factor , find numbers , , , and such that . There are 3 cases here:
a. If , then and .
b. If , find such that , letting and .
c. If , find and such that , letting and .
Now that we have , construct , , , and such that where . Repeat this procedure until .
The whole flow of the program looks like this:
So we factor
n, and for each prime factor, find its four-square decomposition using
combine them pairwise. For its part,
foursquare' does some magic to find initial values for our 4 numbers
and shuffles them off to
reduce to get the sum of their squares to be exactly equal to
p instead of
a multiple of
I also defined the operator
|> as backwards function application.
It makes more sense to me to push a value through a series
of functions than to have to read all my expressions inside out.
Alright, now I’m going to go through piece by piece and fill in missing definitions.
The easy parts
Factoring is probably the second Haskell program you ever wrote (the first probably also beginning with “factor”). Here it is from scratch, for fun:
And yes, there are more efficient ways to generate primes.
combine is a straighforward realization of Euler’s four-square identity:
I’m also going to need modular exponentiation, to compute :
And a helper for finding the sum of squares of 4 numbers:
Before we go on, let’s check that
*Main> let x = (1, 2, 3, 4) *Main> let y = (5, 6, 7, 8) *Main> sumOfSquares x 30 *Main> sumOfSquares y 174 *Main> sumOfSquares (combine x y) 5220 *Main> 30*174 5220
Let’s do that 100 more times.
*Main> quickCheck (\x y -> (sumOfSquares x) * (sumOfSquares y) == sumOfSquares(combine x y)) +++ OK, passed 100 tests.
I freaking love
Odd primes congruent to 1 mod 4
Now to fill in the missing parts of
foursquare'. Here’s the first clause:
Here we have to find such that . In other words, we’re looking for a square root of . By Fermat’s little theorem, if then , which means that its square root, , is congruent to . If we can find one such that , then its square root, , is the we’re after. Notice this only works because is an integer.
Well luckily it turns out that half of the time, , so if we just try numbers sequentially we’re liable to find one pretty quickly. It also turns out that the smallest such is always a prime number, so we can narrow down the search that way.
The code is below. We’re just trying prime numbers until one of them satisifies .
Odd primes congruent to 3 mod 4
Here’s the next clause of
This case is a little more difficult. We’re looking for and such that . Equivalently, we’re looking for a that is a square root of . We’re guaranteed that there is some such that has a square root , but I’ll refer you to the the full proof for the details on why this is. For our purposes, all we need to do is try different values of sequentially and check whether they produce a square root. That’s easy to check, at least: if , then is a square root of , if it has one. Here’s a quick proof:
since by Fermat’s little theorem. (This doesn’t always produce a square root of since it might instead be a square root of .)
The proof gets a little hand-wavy on this part, but it turns out that finding an such that has a square root mod is pretty easy. It points out that -2 has a square root mod for all , which is already half of the cases.
Anyway, here’s the code:
The reduce phase
Now that we have , we want to somehow construct a new set of numbers , , , and such that where . Then we can repeat the procedure until .
If is even, then is even, meaning 0, 2 or all 4 of the numbers are even. Rearranging them according to their remainder mod 2, we can get it so that and are both even. Then we can divide through by 2 and get
and we have the reduction we need. In code:
making use of the convenience functions
If is odd, we can replace each of the 4 numbers by their “absolute least residue” mod . All this means is, if , we replace it with , which reduces its absolute value without changing its meaning mod . So let be the absolute least residue of and so on. Since all of them are smaller than , their squares are less than and the sum of their squares is less than . The sum of their squares is still , so the sum must be equal to for some .
Now we can use
combine to construct the product
combine function is written in such a way that each of the terms , , , and
will be divisible by . This is easy to see by inspecting each term and remembering that
So we can divide out from each of the terms to get a product equal to , and we have the
reduction we need.
Here’s the complete code for
And that completes the construction.
Let’s try it out:
*Main> foursquare 2013 (10,12,40,13) *Main> foursquare 20131114 (4455,533,0,0) *Main> foursquare 1729 (32,-22,-11,10) *Main> quickCheck (\n -> n >= 0 ==> sumOfSquares (foursquare n) == n) +++ OK, passed 100 tests.
So yeah, this is pretty useless, but it was fun to see it actually work. The code is available in this gist if you want to play around with it.
blog comments powered by Disqus