Finite MTerms weight

Proved

D1Bound5.finiteMTerms_weight

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

diophantine-tuplesnumber-theory

The complete finite row certificate; it requires no norm or analytic assumption. In row zero the exact sum is38400, in the other rows169728.

Preamble

import Mathlib.Algebra.BigOperators.Fin
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_FiniteMMatrix_Definitions

Formal statement

section
namespace D1Bound5






















theorem _root_.D1Bound5.finiteMTerms_weight (i : Fin 4) :
    (∑ j : Fin 3, ((finiteMTerms i j.succ).map finiteMTermWeight).sum) ≤ 169728 := by sorry






end D1Bound5
end

Source

D1Bound5/FiniteMMatrix.lean, lines 150-154, SHA-256 8af7f9699b9fc84a48e57a25795d84c9aefe6f4ade8e20a65b9b82216db511c9. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph