Finite QDivided Matrix root height

Proved

D1Bound5.finiteQDividedMatrix_root_height

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

diophantine-tuplesnumber-theory

Every one of the five actual rows satisfies the same root-column height bound. The selected nonzero integral row can therefore be used without imposing a separate height certificate.

Preamble

import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Analysis.Complex.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.GCongr
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_FiniteQMatrix_Definitions

Formal statement

section
namespace D1Bound5




theorem _root_.D1Bound5.finiteQDividedMatrix_root_height
    (a b s t c : ℂ) (T C : ℝ) (hT : 0 ≤ T) (hC : 0 ≤ C)
    (ha : ‖a‖ ≤ T) (hb : ‖b‖ ≤ T) (hs : ‖s‖ ≤ T) (ht : ‖t‖ ≤ T)
    (hc : ‖c‖ ≤ C) (hTC : 1 ≤ T*C) (i : Fin 5) :
    (∑ j : Fin 4, ‖finiteQDividedMatrix a b s t c i j.succ‖) ≤ 36*T^3*C := by sorry

end D1Bound5
end

Source

D1Bound5/FiniteQHeight.lean, lines 41-55, SHA-256 86865cf236ac82f61de86bc28514d9e3b24a1d93eff23574b7cf2a6d0efa3d7e. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph