Exclusion of degree at least two — Theorem 9, case V
Opendiophantine_degree_ge_two_case_fivediophantine-equationsnumber-theory
Assume an ordered Diophantine triple of degree at least two, the global bound from Proposition 5, and the interval hypothesis $$$4a^2b^3<c<180.45,b^3/a20ac<3609b^31\le a\le 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_five_quintuple instead: https://prove2.me/theorems/95666c13-d5ac-4753-b42a-5d701a465b0f.
Preamble
import Definitions.Def_diophantine_descent set_option autoImplicit false open DiophantineDescent
Formal statement
theorem diophantine_degree_ge_two_case_five (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 ^ 2 * b ^ 3 < c) (hhi : a * c * 20 < 3609 * 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).