# Documentation

Archive.ZagierTwoSquares

# Zagier's "one-sentence proof" of Fermat's theorem on sums of two squares #

"The involution on the finite set S = {(x, y, z) : ℕ × ℕ × ℕ | x ^ 2 + 4 * y * z = p} defined by

(x, y, z) ↦ (x + 2 * z, z, y - x - z) if x < y - z
(2 * y - x, y, x - y + z) if y - z < x < 2 * y
(x - 2 * y, x - y + z, y) if x > 2 * y


has exactly one fixed point, so |S| is odd and the involution defined by (x, y, z) ↦ (x, z, y) also has a fixed point." — Don Zagier

This elementary proof (Nat.Prime.sq_add_sq') is independent of Nat.Prime.sq_add_sq in Mathlib.NumberTheory.SumTwoSquares, which uses the unique factorisation of ℤ[i]. For a geometric interpretation of the piecewise involution (Zagier.complexInvo) see Moritz Firsching's MathOverflow answer.

def Zagier.zagierSet (k : ) :

The set of all triples of natural numbers (x, y, z) satisfying x * x + 4 * y * z = 4 * k + 1.

Instances For
theorem Zagier.zagierSet_lower_bound (k : ) [hk : Fact (Nat.Prime (4 * k + 1))] {x : } {y : } {z : } (h : (x, y, z) ) :
0 < x 0 < y 0 < z
theorem Zagier.zagierSet_upper_bound (k : ) [hk : Fact (Nat.Prime (4 * k + 1))] {x : } {y : } {z : } (h : (x, y, z) ) :
x k + 1 y k z k
theorem Zagier.zagierSet_subset (k : ) [hk : Fact (Nat.Prime (4 * k + 1))] :
Set.Ioc 0 (k + 1) ×ˢ Set.Ioc 0 k ×ˢ Set.Ioc 0 k
noncomputable instance Zagier.instFintypeElemProdNatZagierSet (k : ) [hk : Fact (Nat.Prime (4 * k + 1))] :
def Zagier.obvInvo (k : ) :

The obvious involution (x, y, z) ↦ (x, z, y).

Instances For
theorem Zagier.obvInvo_sq (k : ) :
= 1
theorem Zagier.sq_add_sq_of_nonempty_fixedPoints (k : ) (hn : ) :
a b, a ^ 2 + b ^ 2 = 4 * k + 1

If obvInvo k has a fixed point, a representation of 4 * k + 1 as a sum of two squares can be extracted from it.

The complicated involution, defined piecewise according to how x compares with y - z and 2 * y.

Instances For
theorem Zagier.complexInvo_sq (k : ) [hk : Fact (Nat.Prime (4 * k + 1))] :
= 1

complexInvo k is indeed an involution.

theorem Zagier.eq_of_mem_fixedPoints (k : ) [hk : Fact (Nat.Prime (4 * k + 1))] {t : ↑()} (mem : ) :
t = (1, 1, k)

Any fixed point of complexInvo k must be (1, 1, k).

The singleton containing (1, 1, k).

Instances For
theorem Zagier.card_fixedPoints_eq_one (k : ) [hk : Fact (Nat.Prime (4 * k + 1))] :

complexInvo k has exactly one fixed point.

theorem Nat.Prime.sq_add_sq' {p : } [h : Fact ()] (hp : p % 4 = 1) :
a b, a ^ 2 + b ^ 2 = p

Fermat's theorem on sums of two squares (Wiedijk #20). Every prime congruent to 1 mod 4 is the sum of two squares, proved using Zagier's involutions.