Full ring descent denominator norm sq ge seven

Proved

D1Bound5.full_ring_descent_denominator_norm_sq_ge_seven

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

diophantine-tuplesnumber-theory

The denominator estimate needed for small-pair descent holds in the full integer ring. The zero radicand is explicitly the exceptional case; no smallness, strict norm ordering, or unit classification is assumed.

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.full_ring_descent_denominator_norm_sq_ge_seven
    {K : Type*} [Field K] [NumberField K] [NumberField.IsTotallyComplex K]
    (hK : finrank ℚ K = 2) (phi : K →+* ℂ)
    (a b r : 𝓞 K) (ha : a ≠ 0) (hb : b ≠ 0)
    (hab : a * b + 1 ≠ 0) (hr : r ^ 2 = a * b + 1) :
    7 ≤ ‖2 * phi (a : K) * phi (b : K) + 1‖ ^ 2 := by sorry

end D1Bound5
end

Source

D1Bound5/DescentDenominator.lean, lines 57-83, SHA-256 4ea39dd9345b8a90b2de77132f93bba0d65366b0fcc68d814f94aaf0c70fdf97. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph