Exclusion of degree at least two — Theorem 9, case II
Opendiophantine_degree_ge_two_case_twodiophantine-equationsnumber-theory
Assume an ordered Diophantine triple of degree at least two, the global bound from Proposition 5, and the interval hypothesis $$$4a^{1/2}b^{3/2}<c\le 4ab^2$.$$ 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_two_quintuple instead: https://prove2.me/theorems/ca60c3f3-bdc9-406e-9e4d-30a33362a0fd.
Preamble
import Definitions.Def_diophantine_descent set_option autoImplicit false open DiophantineDescent
Formal statement
theorem diophantine_degree_ge_two_case_two (a b c n : Nat) (ht : Triple a b c)
(hn : 2 ≤ n) (hd : HasDegree a b c n)
(hglob : a * c < 67700000000000000000000000) (hlo : 16 * a * b ^ 3 < c ^ 2) (hhi : c ≤ 4 * a * b ^ 2) : 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).