Discrete unit pair symmetric obstruction

Proved

D1Bound5.discrete_unit_pair_symmetric_obstruction

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

diophantine-tuplesnumber-theory

Symmetric form of the obstruction: both entries extend {-1,1} and both signs of their product plus one are squares. Ordering is supplied internally, so no mutation or artificial tuple extension is used.

Preamble

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Analysis.Complex.Norm
import Mathlib.Data.Finset.Card
import Mathlib.Data.Int.GCD
import Mathlib.LinearAlgebra.Dimension.Free
import Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
import Mathlib.NumberTheory.NumberField.Norm
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination

Formal statement

section
open scoped NumberField
open Module

namespace D1Bound5








theorem _root_.D1Bound5.discrete_unit_pair_symmetric_obstruction
    {R : Type*} [CommRing R] (f : R →+* ℂ)
    (hdiscrete : ∀ z : R, z ≠ 0 → 1 ≤ ‖f z‖)
    (a b : R) (hA : 3 ≤ ‖f a‖) (hB : 3 ≤ ‖f b‖)
    (ham : ∃ x : R, x ^ 2 = 1 - a) (hap : ∃ y : R, y ^ 2 = 1 + a)
    (hbm : ∃ x : R, x ^ 2 = 1 - b) (hbp : ∃ y : R, y ^ 2 = 1 + b)
    (habm : ∃ v : R, v ^ 2 = 1 - a * b)
    (habp : ∃ w : R, w ^ 2 = 1 + a * b) : False := by sorry



end D1Bound5
end

Source

D1Bound5/UnitPairSymmetric.lean, lines 102-124, SHA-256 695ec9ac631f60966fa825624a829a3fc795041a1c15a2f07c5f310997593968. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph