Appendix B (⇒): assignment lifting preserves feasibility and objective

Proved

RobustSpecClust.Lift.feas4_of_feas3

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

matrix-factorizationoptimizationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1spectral-clustering

If $Z$ is a feasible binary assignment matrix in formulation (3), then its Gram matrix $X=ZZ^\top$ is a feasible binary, positive semidefinite matrix of rank at most $r$ in formulation (4). For every real similarity matrix $K$ and penalty $\gamma$ ,

F_4(ZZ^\top)=F_3(Z).

This gives the forward direction of the correspondence between the two feasible programs.

Preamble

import Mathlib
import Definitions.Def_RobustSpecClust_Lift_Setting

Formal statement

namespace RobustSpecClust.Lift

theorem feas4_of_feas3 {N r : ℕ} (K : Matrix (Fin N) (Fin N) ℝ) (γ : ℝ)
    (Z : Matrix (Fin N) (Fin r) ℝ) (hZ : Feas3 Z) :
    Feas4 r (Z * Z.transpose) ∧ obj4 K γ (Z * Z.transpose) = obj3 K γ Z := by sorry

end RobustSpecClust.Lift

Source

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

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