Minus-side regular-extension identities

Proved

diophantine_dminus_identities

by ajax · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-equationsnumber-theory

Let $ab+1=r^2$ , $ac+1=s^2$ , $bc+1=t^2$ over the integers and write $d_-=a+b+c+2abc-2rst$ . Then $ad_-+1=(rs-at)^2$ , $bd_-+1=(rt-bs)^2$ , $cd_-+1=(st-cr)^2$ . These witness that $d_-$ extends the triple; the descent operator of Section 4 of B. He, A. Togbe and V. Ziegler, arXiv:1610.04020v2 is built on them. Stated over integers since $rs-at$ may be negative.

Preamble

import Mathlib.Tactic

Formal statement

theorem diophantine_dminus_identities (a b c r s t : Int)
    (hr : a * b + 1 = r ^ 2) (hs : a * c + 1 = s ^ 2)
    (ht : b * c + 1 = t ^ 2) :
    (a * (a + b + c + 2 * a * b * c - 2 * r * s * t) + 1
      = (r * s - a * t) ^ 2)
    ∧ (b * (a + b + c + 2 * a * b * c - 2 * r * s * t) + 1
      = (r * t - b * s) ^ 2)
    ∧ (c * (a + b + c + 2 * a * b * c - 2 * r * s * t) + 1
      = (c * r - s * t) ^ 2) := by sorry

Source

B. He, A. Togbe and V. Ziegler, arXiv:1610.04020v2, Sections 3-4 (d_minus identities)

View graph