Exclusion of sextuples with all absolute values at least three

Proved

D1Bound5.IsD1Tuple.all_large_impossible

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

diophantine-tuplesnumber-theory

Let K be an imaginary quadratic number field, let phi be a complex embedding, and let t be a Diophantine sextuple in its full ring of integers. Assume that the absolute values of the images of its entries are nondecreasing. Such a sextuple is impossible if the first absolute value is at least 3.

The sextuple consists of distinct nonzero algebraic integers, and the product of any two distinct entries plus one is a square in the full ring of integers. Equal absolute values are permitted. This is one of the exhaustive branches used to establish the cardinality bound.

Preamble

import Definitions.Def_D1Bound5_IsD1Tuple
import Definitions.Def_D1Bound5_MainStatement
import Mathlib.Analysis.Complex.Basic

open scoped NumberField
open Module D1Bound5

Formal statement

theorem D1Bound5.IsD1Tuple.all_large_impossible
    {K : Type*} [Field K] [NumberField K] [NumberField.IsTotallyComplex K]
    (hK : finrank ℚ K = 2) (phi : K →+* ℂ)
    (a : Fin 6 → 𝓞 K) (ha : IsD1Tuple a)
    (hmon : Monotone (fun i => ‖phi (a i : K)‖))
    (hA : 3 ≤ ‖phi (a 0 : K)‖) : False := by sorry

Source

D1Bound5/AllLargeImpossible.lean, D1Bound5.IsD1Tuple.all_large_impossible, lines 14-19; exact source SHA-256 33a0330c203e78ef360d3145b58a19fb19c43490eaed1fa7a331623489af59e0. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph