Exclusion of a degenerate first pair in an ordered sextuple

Proved

D1Bound5.IsD1Tuple.degenerate_first_pair_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 product of the first two entries plus one is zero.

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.degenerate_first_pair_impossible
    {K : Type*} [Field K] [NumberField K] [NumberField.IsTotallyComplex K]
    (hK : finrank ℚ K = 2) (phi : K →+* ℂ)
    (t : Fin 6 → 𝓞 K) (ht : IsD1Tuple t)
    (hmon : Monotone (fun i => ‖phi (t i : K)‖))
    (hprod : t 0*t 1+1=0) : False := by sorry

Source

D1Bound5/DegeneratePairImpossible.lean, D1Bound5.IsD1Tuple.degenerate_first_pair_impossible, lines 83-88; exact source SHA-256 449a3a0eb81ab63cbb073585d13a396c6886de6c7e8f6b4565307a657ed38f67. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph