Congruent Number

A natural number $n$ is called a congruent number if there exists a right triangle with rational sides $a$, $b$, and hypotenuse $c$ such that the area of the triangle is $\frac{1}{2}ab = n$.

References:

• Wikipedia (Congruent number)
• Wikipedia (Tunnell's theorem)
• Keith Conrad's note

def CongruentNumber.congruentNumber (n : ℕ) : Prop

Equations

• CongruentNumber.congruentNumber n = ∃ (a : ℚ) (b : ℚ) (c : ℚ), a ^ 2 + b ^ 2 = c ^ 2 ∧ ↑n = 2⁻¹ * a * b

theorem CongruentNumber.not_congruentNumber_1 : ¬congruentNumber 1

1 is not a congruent number, as proved by Fermat via infinite descent.

theorem CongruentNumber.congruentNumber_5 : congruentNumber 5

theorem CongruentNumber.congruentNumber_6 : congruentNumber 6

theorem CongruentNumber.congruentNumber_7 : congruentNumber 7

theorem CongruentNumber.congruentNumber_157_zagier : congruentNumber 157

def CongruentNumber.A (n : ℕ) : Set (ℤ × ℤ × ℤ)

Equations

• CongruentNumber.A n = {(x, y, z) : ℤ × ℤ × ℤ | ↑n = 2 * x ^ 2 + y ^ 2 + 32 * z ^ 2}

def CongruentNumber.B (n : ℕ) : Set (ℤ × ℤ × ℤ)

Equations

• CongruentNumber.B n = {(x, y, z) : ℤ × ℤ × ℤ | ↑n = 2 * x ^ 2 + y ^ 2 + 8 * z ^ 2}

def CongruentNumber.C (n : ℕ) : Set (ℤ × ℤ × ℤ)

Equations

• CongruentNumber.C n = {(x, y, z) : ℤ × ℤ × ℤ | ↑n = 8 * x ^ 2 + 2 * y ^ 2 + 64 * z ^ 2}

def CongruentNumber.D (n : ℕ) : Set (ℤ × ℤ × ℤ)

Equations

• CongruentNumber.D n = {(x, y, z) : ℤ × ℤ × ℤ | ↑n = 8 * x ^ 2 + 2 * y ^ 2 + 16 * z ^ 2}

theorem CongruentNumber.Tunnell_odd (n : ℕ) (hsqf : Squarefree n) (hodd : Odd n) : congruentNumber n → 2 * (A n).ncard = (B n).ncard

Tunnell's theorem (necessary condition) for odd squarefree congruent numbers.

theorem CongruentNumber.Tunnell_even (n : ℕ) (hsqf : Squarefree n) (heven : Even n) : congruentNumber n → 2 * (C n).ncard = (D n).ncard

Tunnell's theorem (necessary condition) for even squarefree congruent numbers.

theorem CongruentNumber.Tunnell_odd_converse (n : ℕ) (hsqf : Squarefree n) (hodd : Odd n) : 2 * (A n).ncard = (B n).ncard → congruentNumber n

Tunnell's theorem (sufficient condition assuming BSD) for odd squarefree congruent numbers.

theorem CongruentNumber.Tunnell_even_converse (n : ℕ) (hsqf : Squarefree n) (heven : Even n) : 2 * (C n).ncard = (D n).ncard → congruentNumber n

Tunnell's theorem (sufficient condition assuming BSD) for even squarefree congruent numbers.