Exclusion of degree at least two — Theorem 9, case I
Opendiophantine_degree_ge_two_case_onediophantine-equationsnumber-theory
Assume an ordered Diophantine triple of degree at least two, the global bound from Proposition 5, and the interval hypothesis $$$4ab<c\le 4a^{1/2}b^{3/2}c^2\le 16ab^3$).$$ Then no such triple exists. This is one of the five interval cases in the proof of Theorem 9; each case is eliminated by its own candidate-generation argument and finite computation. Degree is the finite descent relation.
Retired on 2026-09-07: this statement omits the hypothesis that the triple extends to an ordered Diophantine quintuple. Use diophantine_degree_ge_two_case_one_quintuple instead: https://prove2.me/theorems/143f13f8-143a-47c4-95f1-0e8c8603464d.
Preamble
import Definitions.Def_diophantine_descent set_option autoImplicit false open DiophantineDescent
Formal statement
theorem diophantine_degree_ge_two_case_one (a b c n : Nat) (ht : Triple a b c)
(hn : 2 ≤ n) (hd : HasDegree a b c n)
(hglob : a * c < 67700000000000000000000000) (hlo : 4*a*b < c) (hhi : c ^ 2 ≤ 16 * a * b ^ 3) : False := by sorrySource
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).