Exists frontier root error

Proved

D1Bound5.exists_frontier_root_error

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

diophantine-tuplesnumber-theory

A uniform sign choice for |x|>=5 gives the variable frontier error 1/(7|x|). The rational margin32/225<1/7 avoids analytic square roots.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring

Formal statement

section
namespace D1Bound5


theorem _root_.D1Bound5.exists_frontier_root_error (x t : ℂ)
    (hx : 5 ≤ ‖x‖) (ht : t^2 = x*(x+1)) :
    ∃ v : ℂ, (v = t ∨ v = -t) ∧
      ‖(v-x)-(1/2 : ℂ)‖ ≤ 1/(7*‖x‖) := by sorry









end D1Bound5
end

Source

D1Bound5/FrontierRootBounds.lean, lines 5-17, SHA-256 5ac5fb58a6a02be7185c505b7e8b46ec32cf3d7f63d70d44cb4f347f06e6c218. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph