For a fundamental discriminant $d>0$ , $t^2-du^2=4$ has a solution with $t,u>0$

Proved

ClassNumberFormula.pell_four_solvable

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

class-number-formulanumber-theory

Let $d > 0$ be a fundamental discriminant. Then there are positive integers $t, u$ with

t^2 - d\,u^2 = 4 .

The source takes such a solution, with $u$ minimal, to define $\varepsilon = \frac12(t + u\sqrt d)$ ; this milestone records that the solution exists, so that $\varepsilon$ is well defined.

Preamble

import Mathlib
import Definitions.Def_ClassNumberFormula_Kronecker
open NumberField NumberField.InfinitePlace NumberField.Units Filter Topology Real

Formal statement

namespace ClassNumberFormula

theorem pell_four_solvable (d : ℤ) (hd : IsFundamentalDiscriminant d) (hpos : 0 < d) :
    ∃ t u : ℕ, 0 < t ∧ 0 < u ∧ (t : ℤ) ^ 2 - d * (u : ℤ) ^ 2 = 4 := by sorry

end ClassNumberFormula

Source

Wikipedia, "Class number formula" (revision oldid=1366411311), https://en.wikipedia.org/w/index.php?title=Class_number_formula&oldid=1366411311, section "Dirichlet class number formula" ("For d > 0, let t > 0, u > 0 be the solution to the Pell equation

t^2 - du^2 = 4

for which u is smallest")

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

For a fundamental discriminant d>0d>0d>0, t2−du2=4t^2-du^2=4t2−du2=4 has a solution with t,u>0t,u>0t,u>0

For a fundamental discriminant $d>0$ , $t^2-du^2=4$ has a solution with $t,u>0$