Exclusion of degree at least two — Theorem 9, case I

Open

diophantine_degree_ge_two_case_one_quintuple

by xuanji · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-equationsnumber-theory

Let $a<b<c$ be an ordered Diophantine triple of degree at least two that extends to an ordered Diophantine quintuple $f$ with $f_0=a$ , $f_1=b$ , $f_2=c$ . Assume the global bound $ac<6.77\cdot 10^{25}$ and the interval hypothesis

4ab<c\le 4a^{1/2}b^{3/2}\quad\text{(squared: }c^2\le 16ab^3\text{)}.

Then no such configuration exists. This is Case I of the five-interval split in the proof of Theorem 9; it is eliminated by its own candidate-generation argument and finite computation. Formalization note: degree is the finite descent relation HasDegree, and the quintuple extension is witnessed by explicit Quintuple and Ordered hypotheses with f 0 = a, f 1 = b, f 2 = c.

Preamble

import Definitions.Def_diophantine_descent
set_option autoImplicit false
open DiophantineDescent

Formal statement

theorem diophantine_degree_ge_two_case_one_quintuple (a b c n : Nat) (f : Fin 5 → Nat) (ht : Triple a b c)
    (hn : 2 ≤ n) (hd : HasDegree a b c n)
    (hq : Quintuple f) (ho : Ordered f) (ha : f 0 = a) (hb : f 1 = b) (hc : f 2 = c)
    (hglob : a * c < 67700000000000000000000000) (hlo : 4*a*b < c) (hhi : c ^ 2 ≤ 16 * a * b ^ 3) : False := by sorry

Source

Bo He, Alain Togbé, Volker Ziegler, There is no Diophantine quintuple, arXiv:1610.04020v2, https://arxiv.org/abs/1610.04020v2; Section 9, proof of Theorem 9 (five-interval split).

View graph