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

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

Tunnell's theorem: Let $A_n$, $B_n$, $C_n$, and $D_n$ be the sets defined as follows:

• $A_n = \{(x, y, z) \in \mathbb{Z}^3 : n = 2x^2 + y^2 + 32z^2\}$
• $B_n = \{(x, y, z) \in \mathbb{Z}^3 : n = 2x^2 + y^2 + 8z^2\}$
• $C_n = \{(x, y, z) \in \mathbb{Z}^3 : n = 8x^2 + 2y^2 + 64z^2\}$
• $D_n = \{(x, y, z) \in \mathbb{Z}^3 : n = 8x^2 + 2y^2 + 16z^2\}$

If $n$ is a squarefree congruent number, then:

• If $n$ is odd, then $2 |A_n| = |B_n|$.
• If $n$ is even, then $2 |C_n| = |D_n|$.

Converse is true under the BSD conjecture.

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}

Tunnell's theorem.

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

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

Converse of Tunnell's theorem.

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

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