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 : ℕ) : Set (ℕ × ℕ × ℕ)

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

Equations

• Zagier.zagierSet k = {t : ℕ × ℕ × ℕ | t.1 * t.1 + 4 * t.2.1 * t.2.2 = 4 * k + 1}

theorem Zagier.zagierSet_lower_bound (k : ℕ) [hk : Fact (Nat.Prime (4 * k + 1))] {x y z : ℕ} (h : (x, y, z) ∈ Zagier.zagierSet k) : 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) ∈ Zagier.zagierSet k) : x ≤ k + 1 ∧ y ≤ k ∧ z ≤ k

theorem Zagier.zagierSet_subset (k : ℕ) [hk : Fact (Nat.Prime (4 * k + 1))] : Zagier.zagierSet k ⊆ 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))] : Fintype ↑(Zagier.zagierSet k)

Equations

• Zagier.instFintypeElemProdNatZagierSet k = ⋯.fintype

def Zagier.obvInvo (k : ℕ) : Function.End ↑(Zagier.zagierSet k)

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

Equations

• Zagier.obvInvo k ⟨(x_1, y, z), h⟩ = ⟨(x_1, z, y), ⋯⟩

theorem Zagier.obvInvo_sq (k : ℕ) : Zagier.obvInvo k ^ 2 = 1

theorem Zagier.sq_add_sq_of_nonempty_fixedPoints (k : ℕ) (hn : (Function.fixedPoints (Zagier.obvInvo k)).Nonempty) : ∃ (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.

def Zagier.complexInvo (k : ℕ) : Function.End ↑(Zagier.zagierSet k)

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

Equations

• Zagier.complexInvo k ⟨(x_1, y, z), h⟩ = ⟨if x_1 + z < y then (x_1 + 2 * z, z, y - x_1 - z) else if 2 * y < x_1 then (x_1 - 2 * y, x_1 + z - y, y) else (2 * y - x_1, y, x_1 + z - y), ⋯⟩

theorem Zagier.complexInvo_sq (k : ℕ) [hk : Fact (Nat.Prime (4 * k + 1))] : Zagier.complexInvo k ^ 2 = 1

complexInvo k is indeed an involution.

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

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

def Zagier.singletonFixedPoint (k : ℕ) : Finset ↑(Zagier.zagierSet k)

The singleton containing (1, 1, k).

Equations

• Zagier.singletonFixedPoint k = {⟨(1, 1, k), ⋯⟩}

theorem Zagier.card_fixedPoints_eq_one (k : ℕ) [hk : Fact (Nat.Prime (4 * k + 1))] : Fintype.card ↑(Function.fixedPoints (Zagier.complexInvo k)) = 1

complexInvo k has exactly one fixed point.

theorem Nat.Prime.sq_add_sq' {p : ℕ} [h : Fact (Nat.Prime p)] (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.