Pair seed root norm le

Proved

D1Bound5.pair_seed_root_norm_le

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

diophantine-tuplesnumber-theory

Every root needed for the radius-33 seed search has norm at most 132. This deliberately loose bound keeps the finite search small and uniform.

Preamble

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Prod
import Mathlib.Data.Int.Interval
import Mathlib.Data.Int.Sqrt
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Definitions.Def_D1Bound5_Coordinates_Definitions

Formal statement

section
namespace D1Bound5
open QuadInt






theorem _root_.D1Bound5.pair_seed_root_norm_le {tau nu : ℤ}
    (hd : 0 < discriminant tau nu) (a z q : QuadInt tau nu)
    (ha : a.norm ≤ 8) (hz : z.norm ≤ 1089) (hq : q*q = a*z+1) :
    q.norm ≤ 132 := by sorry





























end D1Bound5
end

Source

D1Bound5/PairExtensionCore.lean, lines 23-37, SHA-256 d45446b353f1adcd08c1943cfe73040bef48ad11485fc541c7388b34f9e5255f. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph