Appendix B (⇐): Gram rows are zero or unit vectors

Proved

RobustSpecClust.Lift.row_zero_or_unit

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

linear-algebramatrix-factorizationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1spectral-clustering

Suppose $X=GG^\top$ and every entry of $X$ is zero or one. Then every row $g_i$ of $G$ is either the zero vector or a unit vector:

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

This identifies zero rows with potential outliers and constrains nonzero rows before the rotation to assignment coordinates.

Preamble

import Mathlib
import Definitions.Def_RobustSpecClust_Lift_Setting

Formal statement

namespace RobustSpecClust.Lift

theorem row_zero_or_unit {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, G i = 0 ∨ ∑ k, G i k ^ 2 = 1 := by sorry

end RobustSpecClust.Lift

Source

arXiv:1912.07546v3, Appendix B, proof of Proposition 1 (⇐), p. 37, second claim

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