Descent step exists for non-Euler triples

Proved

diophantine_descent_step_exists

by xuanji · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-equationsnumber-theory

Let $a<b<c$ be a non-Euler Diophantine triple. Then one descent step applies: with $r^2=ab+1$ , $s^2=ac+1$ , $t^2=bc+1$ and $m=a+b+c+2abc-2rst$ , we have $0<m<c$ and the increasing rearrangement of $a,b,m$ is again a Diophantine triple. That is, the paper's $\partial_{-1}$ -operator is well defined. This is the hard number-theoretic half of Proposition 3 (Lemma 7); termination is handled separately by induction on the largest entry.

Preamble

import Definitions.Def_diophantine_descent
set_option autoImplicit false
open DiophantineDescent

Formal statement

theorem diophantine_descent_step_exists (a b c : Nat) (h : Triple a b c) (hne : ¬ Euler a b c) :
    ∃ x y z : Nat, Step a b c x y z := by sorry

Source

Bo He, Alain Togbé, Volker Ziegler, There is no Diophantine quintuple, arXiv:1610.04020v2, https://arxiv.org/abs/1610.04020v2; Sections 3-4, Lemma 7 (well-definedness of the descent operator).

View graph