Signed Entry Bounds swap

Proved

D1Bound5.signedEntryBounds_swap

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

diophantine-tuplesnumber-theory

Auxiliary result signedEntryBounds_swap in the proof of the bound five for Diophantine D(1) sets in imaginary quadratic integer rings. The formal statement specifies its hypotheses and conclusion; a mathematical prose description remains to be supplied.

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
import Definitions.Def_D1Bound5_MixedRootMatrixSigns_Definitions

Formal statement

section
namespace D1Bound5



theorem _root_.D1Bound5.signedEntryBounds_swap {R : Type*} [CommRing R]
    (f : R →+* ℂ) (a b r : R) (u v : ℂ) (rho eta : ℝ)
    (h : SignedEntryBounds f a b u v r rho eta) :
    SignedEntryBounds f b a v u r rho eta := by sorry













end D1Bound5
namespace D1Bound5





end D1Bound5
end

Source

D1Bound5/MixedRootMatrixSigns.lean, lines 12-19, SHA-256 2e004ca5529f8e5abf67259e26a8270075f09b04d9c8093e81458a83e3680457. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph