Every Diophantine triple has finite descent degree

Proved

diophantine_triple_finite_degree

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

diophantine-equationsnumber-theory

Every ordered Diophantine triple $a<b<c$ with $ab+1$ , $ac+1$ , $bc+1$ all squares reaches an Euler triple after finitely many descent steps:

\exists n\in\mathbb{N},\quad \deg(a,b,c)=n.

This is the existence part of the classification (it supplies termination of the descent operator), separated from any quintuple context so it can be reused. It does not assert the quantitative bound or uniqueness.

Preamble

import Definitions.Def_diophantine_descent
set_option autoImplicit false
open DiophantineDescent

Formal statement

theorem diophantine_triple_finite_degree (a b c : Nat) (h : Triple a b c) :
    ∃ n : Nat, HasDegree a b c n := by sorry

Source

Bo He, Alain Togbé, Volker Ziegler, There is no Diophantine quintuple, arXiv:1610.04020v2, https://arxiv.org/abs/1610.04020v2; Section 4, Proposition 3 (existence part).

View graph