Prove2Me

Signed parametrization for degree one

Proved
diophantine_degree_one_parametrization

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

diophantine-equationsnumber-theory

Let a,b,ra,b,r be integers with ab+1=r2ab+1=r^2 and let s=±1s=\pm 1. Put d=a+b+2srd=a+b+2sr (the signed form of d−1=a+b±2rd_{-1}=a+b\pm 2r). Then

(r+sa)2=ad+1,(b+sr)2=bd+1,(r+sa)^2=ad+1,\qquad (b+sr)^2=bd+1,

and the regular-quadruple value satisfies

d+(a,d,b)=a+d+b+2adb+2(r+sa)r(b+sr)=4r(r+sa)(b+sr),d_+(a,d,b)=a+d+b+2adb+2(r+sa)r(b+sr)=4r(r+sa)(b+sr),

i.e. c=4r(r±a)(b±r)c=4r(r\pm a)(b\pm r) with correlated signs. Stated over Z\mathbb{Z} to avoid truncated subtraction. This is the structural computation in the proof of Theorem 8; only the ++ case has d≥0d\ge 0.

Formal statement
theorem diophantine_degree_one_parametrization (a b r s : Int)
    (hs : s = 1 ∨ s = -1) (hr : a * b + 1 = r ^ 2) :
    (r + s * a) ^ 2 = a * (a + b + 2 * s * r) + 1 ∧
    (b + s * r) ^ 2 = b * (a + b + 2 * s * r) + 1 ∧
    a + (a + b + 2 * s * r) + b + 2 * a * (a + b + 2 * s * r) * b
      + 2 * (r + s * a) * r * (b + s * r)
      = 4 * r * (r + s * a) * (b + s * r) := by sorry
Source
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 8 (d−1=a+b±2rd_{-1}=a+b\pm 2r, c=d+(a,d−1,b)c=d_+(a,d_{-1},b)).

View graph