Negative integer square dvd trace zero

Proved

D1Bound5.negative_integer_square_dvd_trace_zero

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

diophantine-tuplesnumber-theory

In the trace-zero model, a negative rational integer square has real coordinate divisible by nu. The existing coordinate classification includes all possible roots, including zero-coordinate cases.

Preamble

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Data.Int.Sqrt
import Mathlib.Tactic.Linarith
import Definitions.Def_D1Bound5_Coordinates_Definitions

Formal statement

section
namespace D1Bound5




theorem _root_.D1Bound5.negative_integer_square_dvd_trace_zero {nu : ℤ}
    (z : QuadInt 0 nu) (him : z.im = 0) (hre : z.re < 0)
    (hsquare : ∃ r : QuadInt 0 nu, r * r = z) : nu ∣ z.re := by sorry







end D1Bound5
end

Source

D1Bound5/PairNegativeIntegerObstruction.lean, lines 14-26, SHA-256 099be79d73801fcfb76bdc30024dc74b43ab6bdb2e935fcd75d8e115af902e02. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph