Eisenstein sum squares balanced coordinates

Proved

D1Bound5.eisenstein_sum_squares_balanced_coordinates

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

diophantine-tuplesnumber-theory

All Eisenstein integral solutions of r²+q²=ω are balanced. The proof uses the exact Pell invariant M²-3D²=1 and descent by the integral matrix with entries 2 and ±sqrt(-3), down to 81 checked coordinate cases.

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.IntervalCases
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Definitions.Def_D1Bound5_Coordinates_Definitions

Formal statement

section
namespace D1Bound5
open QuadInt












theorem _root_.D1Bound5.eisenstein_sum_squares_balanced_coordinates (x y u v : ℤ)
    (hR : x^2-y^2+u^2-v^2 = 0)
    (hI : 2*x*y+y^2+2*u*v+v^2 = 1) :
    (u = y ∧ v = x) ∨ (u = -y ∧ v = -x) := by sorry

end D1Bound5
end

Source

D1Bound5/EisensteinPellDescent.lean, lines 65-149, SHA-256 cd2aa636e64bfd71d3cf36b1229109297e3ce100e0b6bdea085db37182ddca75. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph