Quadratic Reciprocity and (p^2-1)/8

The law of quadratic reciprocity. The jewel in the crown of mathematics! Still not proved in Lean!

Clara List and Sangwoo Jo were thinking about this today. They formalised the statement. There are two “supplements” to the law, describing when -1 and 2 are squares mod p. For the case p=2 they used the dreaded version

\left(\frac{2}{p}\right)=(-1)^{\frac{p^2-1}{8}}

which they obtained from a reliable source. Who even came up with that way of expressing what’s going on? Does it ever help? What’s wrong with just writing that it’s +1 if p\equiv 1 or 7 mod 8, and -1 otherwise? When I’ve lectured the basic number theory course at Imperial, it’s this latter statement that comes out in the wash.

So the ring tactic came to the rescue:


import tactic.ring 

lemma quad_res_two_case_three (n : ℕ) : n % 8 = 3 → (n ^ 2 - 1) / 8 % 2 = 1 :=
begin
  intro H,
  have H2 := nat.mod_add_div n 8,
  rw H at H2,
  rw ←H2,
  suffices : ∀ t : ℕ, ((3 + 8 * t) ^ 2 - 1) / 8 % 2 = 1,
    exact this (n/8),
  intro t,
  have H3 : (1 + 2 * (4*t^2 + 3*t)) % 2 = 1,
    rw nat.add_mul_mod_self_left,exact dec_trivial,
  suffices : ((3 + 8 * t) ^ 2 - 1) / 8 = (1 + 2 * (4 * t ^ 2 + 3 * t)),
    rwa this,
  suffices : ((3 + 8 * t) ^ 2 - 1) = 8 * (1 + 2 * (4 * t ^ 2 + 3 * t)),
    rw this,
  rw nat.mul_div_cancel_left _ (show 8 > 0, from dec_trivial),
  ring
end 

I had to write three more of these but I leave them as exercises (or you can find them in our UROP project repo here in the “M3P14” directory).

So what’s going on in this code? Well, we’d like to use the ring tactic to make this easily, unfortunately it’s an assertion about naturals and it involves both subtraction and division, neither of which are defined to be what mathematicians think of them as, so we have to be careful. In particular we can’t just apply ring and hope it will work.

Unsurprisingly, the first step is to write n as 8t+3, reducing the goal to

((3 + 8 * t) ^ 2 - 1) / 8 % 2 = 1

The next trick is to observe that (1 + 2 * (4*t^2 + 3*t)) % 2 = 1 because the thing we’re reducing mod 2 is 1 plus something even. This reduces us to proving

((3 + 8 * t) ^ 2 - 1) / 8 = (1 + 2 * (4 * t ^ 2 + 3 * t))

but ring still won’t do this because we have an integer division here. However nat.mul_div_cancel_left is that if n>0 then n * m / n = m, meaning that it suffices to prove

(3 + 8 * t) ^ 2 - 1 = 8 * (1 + 2 * (4 * t ^ 2 + 3 * t))

and ring is smart enough to know that the last subtraction is not a problem, and closes our goal.

Advertisements

About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.
This entry was posted in Learning Lean, number theory. Bookmark the permalink.

One Response to Quadratic Reciprocity and (p^2-1)/8

  1. Pingback: Resumen de lecturas compartidas durante julio de 2018 | Vestigium

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s