Discrete unit pair symmetric ordered obstruction

Proved

D1Bound5.discrete_unit_pair_symmetric_ordered_obstruction

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

diophantine-tuplesnumber-theory

In a discrete complex ring image, the four square conditions of the ordered symmetric-five argument are impossible once both moduli are at least three. In particular no root-nonvanishing hypothesis is needed.

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_ordered_obstruction
    {R : Type*} [CommRing R] (f : R →+* ℂ)
    (hdiscrete : ∀ z : R, z ≠ 0 → 1 ≤ ‖f z‖)
    (a b x y v w : R) (hA : 3 ≤ ‖f a‖) (hAB : ‖f a‖ ≤ ‖f b‖)
    (hx : x ^ 2 = 1 - b) (hy : y ^ 2 = 1 + b)
    (hv : v ^ 2 = 1 - a * b) (hw : w ^ 2 = 1 + a * b) : False := by sorry





end D1Bound5
end

Source

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

View graph