Lemma 9: nontrivial column combinations have few zeros

Proved

QAlgorithms.Papers.Independent.Intake100.P43.column_combination_few_zeros

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $1\le n\le m$ , let $M\in M_m(\mathbb C)$ be totally nonsingular, and select $n$ distinct columns using an injection $j\mapsto c_j$ . For coefficients $a_1,\ldots,a_n$ that are not all zero, put $v_i=\sum_j a_j M_{i,c_j}$ . Then

\#\{i:v_i=0\}\le n-1.

Some individual coefficients may vanish. This corrected nontrivial-combination form is the one required by the source’s proof and construction.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P43

Formal statement

noncomputable section

open scoped BigOperators Matrix ComplexConjugate

namespace QAlgorithms.Papers.Independent.Intake100.P43

open QAlgorithms.Papers.Independent.Dependency50.P50 (Bipartite schmidtNumber)

open QAlgorithms.Papers.Independent.Information100.P03 (PureEnsemble)

/-- PDF pp.2–3, Lemma 9, corrected from its proof: printed "any linear
combination" must mean a NONTRIVIAL combination of DISTINCT selected columns.
The all-zero coefficient vector contradicts the literal printed statement.
No requirement that all coefficients be individually nonzero is imposed. -/
theorem column_combination_few_zeros (m n : ℕ) (hn : 1 ≤ n) (hnm : n ≤ m)
    (M : Matrix (Fin m) (Fin m) ℂ) (hM : TotallyNonsingular M)
    (cols : Fin n ↪ Fin m) (c : Fin n → ℂ) (hc : c ≠ 0) :
    (Finset.univ.filter (fun i : Fin m =>
      (∑ j : Fin n, c j * M i (cols j)) = 0)).card ≤ n - 1 := by sorry

end QAlgorithms.Papers.Independent.Intake100.P43

end

Source

On the dimension of subspaces with bounded Schmidt rank, arXiv:0706.0705v1, PDF p. 2, Lemma 9 (proof continues on PDF p.3)

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For all natural numbers $m,n$ with $1\le n\le m$ , every complex $m\times m$ matrix $M$ whose every square submatrix selected by injective row and column lists has nonzero determinant, every injection $\gamma:\{0,\ldots,n-1\}\hookrightarrow\{0,\ldots,m-1\}$ , and every coefficient vector $c\in\mathbb C^n$ with at least one nonzero coefficient, the number of indices $i<m$ satisfying $\sum_{j<n}c_jM_{i,\gamma(j)}=0$ is at most $n-1$ . The condition on square submatrices includes the empty submatrix, whose determinant is $1$ . The subtraction $n-1$ is natural-number subtraction, and $n\ge1$ ensures that it has its usual integer value.

Human review

Endorsed by Shuze Chen · Oct 30, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph