Exclusion of degree at least two — Theorem 9, case IV
Opendiophantine_degree_ge_two_case_fourdiophantine-equationsnumber-theory
Assume an ordered Diophantine triple of degree at least two, the global bound from Proposition 5, and the interval hypothesis $$$4a^{3/2}b^{5/2}<c\le 4a^2b^3c^2>16a^3b^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. Use diophantine_degree_ge_two_case_four_quintuple instead: https://prove2.me/theorems/5d09b2c9-76ca-440d-bb22-ae6a9e44a70b.
Preamble
import Definitions.Def_diophantine_descent set_option autoImplicit false open DiophantineDescent
Formal statement
theorem diophantine_degree_ge_two_case_four (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 ^ 3 * b ^ 5 < c ^ 2) (hhi : c ≤ 4 * a ^ 2 * 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).