Exclusion of degree at least two — Theorem 9, case III
Opendiophantine_degree_ge_two_case_threediophantine-equationsnumber-theory
Assume an ordered Diophantine triple of degree at least two, the global bound from Proposition 5, and the interval hypothesis $$$4ab^2<c\le 4ab^{5/2}c^2\le 16a^2b^5$).$$ 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. Its Case III upper boundary also uses the wrong exponent of a. Use diophantine_degree_ge_two_case_three_quintuple instead: https://prove2.me/theorems/20b664aa-1d67-4836-9703-08d71c01f248.
Preamble
import Definitions.Def_diophantine_descent set_option autoImplicit false open DiophantineDescent
Formal statement
theorem diophantine_degree_ge_two_case_three (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 ^ 2 < c) (hhi : c ^ 2 ≤ 16 * a ^ 2 * b ^ 5) : 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).