CLP Polynomial Method Diagonal Gram Matrix Non-Singular Rank Rigidity

Proved

clp_diagonal_eval_rigid

by Xinyu Xu · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problemslinear-algebra

For any polynomial evaluation matrix M over an AP-free set with non-vanishing diagonal entries and vanishing off-diagonal entries, the algebraic rank of M equals the cardinality of the index set.

Formal statement

import Mathlib.LinearAlgebra.Matrix.Rank
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.LinearAlgebra.Matrix.Diagonal

theorem clp_diagonal_eval_rigid {α : Type*} [Fintype α] [DecidableEq α] {K : Type*} [Field K] [DecidableEq K] (M : Matrix α α K)
    (h_diag : ∀ i : α, M i i ≠ 0)
    (h_off : ∀ i j : α, i ≠ j → M i j = 0) :
    Matrix.rank M = Fintype.card α := by sorry

View graph