One three integer obstruction

Proved

D1Bound5.one_three_integer_obstruction

by tp · Oct 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-tuplesnumber-theory

The integral conic obstruction in lem:pr-one-three. Positivity of both factors already forces k nonzero; no separate irrationality argument is needed.

Preamble

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination

Formal statement

section
namespace D1Bound5





theorem _root_.D1Bound5.one_three_integer_obstruction (delta e f g h k : ℤ)
    (hd : 3 ≤ delta) (hf : f ≠ 0) (hg : g ≠ 0)
    (him : g*h = 3*e*f)
    (hre : 3*e^2-g^2+delta*(h^2-3*f^2) = 8)
    (hk : e*h-f*g = 2*k) : False := by sorry





end D1Bound5
end

Source

D1Bound5/OneThree.lean, lines 20-62, SHA-256 c460b2250b70545a8f61a27e15dc979839749602cbbccd3fc8fadf6e21e02682. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph