Exists root error control

Proved

D1Bound5.exists_root_error_control

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

diophantine-tuplesnumber-theory

Uniform sign selection with a free margin c. The two inequalities are polynomial inequalities in real norms, without division by a possibly zero chosen square root.

Preamble

import Mathlib.Analysis.Complex.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_root_error_control (x t : ℂ) (c : ℝ)
    (hc : 0 ≤ c) (hx : 0 < ‖x‖)
    (hgap : 1 < (1-c^2)*‖x‖) (ht : t^2 = x*(x+1)) :
    ∃ v : ℂ, (v = t ∨ v = -t) ∧
      (1+c)*‖v-x‖ < 1 ∧
      (2*‖x‖*(1+c)^2)*‖(v-x)-(1/2 : ℂ)‖ < 1 := by sorry





end D1Bound5
end

Source

D1Bound5/RootErrorMagnitude.lean, lines 84-137, SHA-256 090472365e3db009e37be35676f898eae037822776991930233fc88ea690af2b. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph