Quad Int — mem disk iff

Proved

D1Bound5.QuadInt.mem_disk_iff

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

diophantine-tuplesnumber-theory

Exact completeness and soundness of disk enumeration. This is valid for every integer cutoff, including an empty negative-cutoff disk.

Preamble

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Data.Finset.Prod
import Mathlib.Data.Int.Interval
import Mathlib.Data.Int.Sqrt
import Mathlib.Tactic.Linarith
import Definitions.Def_D1Bound5_Coordinates_Definitions
import Definitions.Def_D1Bound5_DiskEnumeration_Definitions

Formal statement

section
namespace D1Bound5.QuadInt

variable {tau nu : ℤ}






theorem _root_.D1Bound5.QuadInt.mem_disk_iff (hd : 0 < discriminant tau nu) (M : ℤ) (z : QuadInt tau nu) :
    z ∈ disk tau nu M ↔ z.norm ≤ M := by sorry





end D1Bound5.QuadInt
end

Source

D1Bound5/DiskEnumeration.lean, lines 30-73, SHA-256 d1d1de7efa3c474d4e36936ae73c743f9c42044bc9487e406a2818230fd2ca53. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph