N₂ coefficient bound for oneSmallCutoffRow_23

Proved

D1Bound5.finiteN2CutoffWeights_23_valid

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

diophantine-tuplesnumber-theory

The rational weights finiteN2CutoffWeights_23 give an evaluated N₂ coefficient certificate for cutoff row oneSmallCutoffRow_23. All weights are nonnegative, every coefficient norm satisfies its prescribed weighted bound, and each row’s total weight, multiplied by 101/100, is strictly less than the row’s bound M₂.

Preamble

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Prod
import Mathlib.Data.Int.Interval
import Mathlib.Data.Int.Sqrt
import Mathlib.Data.List.Range
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.GCongr
import Mathlib.Tactic.IntervalCases
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_Coordinates_Definitions
import Definitions.Def_D1Bound5_OneSmallCutoffArithmetic_Definitions_001
import Definitions.Def_D1Bound5_OneSmallN2FixedArithmetic_Definitions

Formal statement

section
namespace D1Bound5
open QuadInt







set_option maxRecDepth 100000
set_option maxHeartbeats 0































































































theorem _root_.D1Bound5.finiteN2CutoffWeights_23_valid :
    FiniteN2FixedBound oneSmallCutoffRow_23 finiteN2CutoffWeights_23 := by sorry







































































































































end D1Bound5
end

Source

D1Bound5/OneSmallN2FixedArithmetic.lean, lines 201-203, SHA-256 164624a5c23628e859c312cd4e25138d33e47f04cca6c8177425d4c89d42a3cd. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph