Appendix B (⇐): distinct nonzero Gram rows are orthogonal

Proved

RobustSpecClust.Lift.rows_eq_or_orthogonal

by mikedeng1 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebrap2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1positive-semidefinitespectral-clustering

Suppose $X=GG^\top$ and every entry of $X$ is zero or one. Any two nonzero rows $g_i,g_j$ of $G$ are either equal or orthogonal:

g_i=g_j\quad\text{or}\quad\sum_{k=1}^{r}(g_i)_k(g_j)_k=0.

Thus the distinct nonzero rows give mutually orthogonal cluster directions. This combines the proof's basis-orthogonality and row-exhaustion claims without fixing its proof-local basis.

Preamble

import Mathlib
import Definitions.Def_RobustSpecClust_Lift_Setting

Formal statement

namespace RobustSpecClust.Lift

theorem rows_eq_or_orthogonal {N r : ℕ} (X : Matrix (Fin N) (Fin N) ℝ)
    (G : Matrix (Fin N) (Fin r) ℝ) (hX : X = G * G.transpose)
    (hbinary : ∀ i j, X i j = 0 ∨ X i j = 1) :
    ∀ i j, G i ≠ 0 → G j ≠ 0 → G i = G j ∨ ∑ k, G i k * G j k = 0 := by sorry

end RobustSpecClust.Lift

Source

arXiv:1912.07546v3, Appendix B, proof of Proposition 1 (⇐), pp. 37–38, orthonormal-basis and row-exhaustion claims

Human review

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

View graph