One three im zero

Proved

D1Bound5.one_three_im_zero

by tp · Oct 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-tuplesnumber-theory

Every common extension of 1 and 3 has zero imaginary coordinate. This theorem is over the exact quadratic-coordinate model; the global full-ring bridge is not assumed or supplied by this declaration.

Preamble

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Definitions.Def_D1Bound5_Coordinates_Definitions

Formal statement

section
namespace D1Bound5







theorem _root_.D1Bound5.one_three_im_zero (tau nu : ℤ)
    (hd : 0 < QuadInt.discriminant tau nu)
    {z r s : QuadInt tau nu} (hr : r*r = z+1) (hs : s*s = 3*z+1) :
    z.im = 0 := by sorry



end D1Bound5
end

Source

D1Bound5/OneThree.lean, lines 64-111, SHA-256 c460b2250b70545a8f61a27e15dc979839749602cbbccd3fc8fadf6e21e02682. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph