Decomposition of the auxiliary function $K$ (Ge–Jin–Zheng Lemma 7; Chen–Li Lemma 4.7)

Proved

MatrixCompletion.NoSpuriousMin.K_decomposition

by Shuze Chen · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

matrix-completionmc-no-spuriousnonconvex-optimization

Let $U$ be any exact factor ( $UU^\top=ZZ^\top$ ), $\Delta = X-U$ , and let $\Omega$ be symmetric. Define $K(X)=\langle\Delta,\nabla^2f(X)[\Delta]\rangle-4\langle\nabla f(X),\Delta\rangle$ . Then, exactly,

K(X)=\bigl\|P_\Omega(\Delta\Delta^\top)\bigr\|_F^2-3\bigl\|P_\Omega(XX^\top-UU^\top)\bigr\|_F^2+\lambda\Bigl(\langle\Delta,\nabla^2R(X)[\Delta]\rangle-4\langle\nabla R(X),\Delta\rangle\Bigr).

This algebraic identity is the heart of the unified landscape analysis: at a local minimum $K(X)\ge 0$ by the optimality conditions, yet the right-hand side is negative unless $\Delta=0$ — a single computation replacing the case analysis of Ge–Lee–Ma's original proof. The identity is pure algebra: no sampling model, no incoherence, no tuning conditions enter.

Formalization Note In Chen–Li's notation the right side is $K_1+K_2+K_3$ with $K_4=0$ since the residual $N$ vanishes in the exact rank- $r$ case; the population/deviation split $K_1+K_2 = \|P_\Omega(\cdot)\|^2$ -form is recombined here.

Preamble

import Definitions.Def_MCNoSpuriousMinModel
open Matrix MatrixCompletion.NoSpuriousMin

Formal statement

theorem MatrixCompletion.NoSpuriousMin.K_decomposition
    {d r : ℕ} (Z X U : Matrix (Fin d) (Fin r) ℝ) (Ω : Finset (Fin d × Fin d))
    (lam α : ℝ)
    (hsym : ∀ i j : Fin d, (i, j) ∈ Ω ↔ (j, i) ∈ Ω)
    (hU : U * Uᵀ = Z * Zᵀ) :
    Kfun Z Ω lam α X U =
      frobSq (projSet Ω ((X - U) * (X - U)ᵀ))
        - 3 * frobSq (projSet Ω (X * Xᵀ - U * Uᵀ))
        + lam * (regHessQF α X (X - U) - 4 * innerM (regGrad α X) (X - U)) := by sorry

Source

Chen, Li 2019, Model-free Nonconvex Matrix Completion: Local Minima Analysis and Applications in Memory-efficient Kernel PCA, JMLR 20(142), https://arxiv.org/abs/1711.01742 (v3) [THE canonical reference: all milestones follow its Section 4], p. 18, Lemma 4.7, eq. (4.6), exact-rank case N = 0 (the K_1+K_2 population/deviation split recombined into ||P_Omega(.)||_F^2 form). Provenance: this is Ge, Jin, Zheng 2017, No Spurious Local Minima in Nonconvex Low Rank Problems, https://arxiv.org/abs/1704.00708, p. 7, Lemma 7, restated by Chen-Li with sampling notation.

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back — MatrixCompletion.NoSpuriousMin.K_decomposition

For every pair of natural numbers $d, r$ (including the degenerate cases $d = 0$ or $r = 0$ , where all sums below are empty and both sides of the claimed equality are $0$ ), every three real $d \times r$ matrices $Z, X, U$ , every finite set $\Omega$ of index pairs $(i,j)$ with $i, j \in \{0, \dots, d-1\}$ , and every pair of real numbers $\lambda, \alpha$ (both completely unrestricted — either may be negative, zero, or positive), the theorem asserts: if

$\Omega$ is symmetric as a set of pairs, i.e. $(i,j) \in \Omega \iff (j,i) \in \Omega$ for all $i, j$ ; and
$U U^\top = Z Z^\top$ exactly (as $d \times d$ matrices),

then the quantity $K$ defined below equals the right-hand side below. Throughout, the following notation abbreviates the definitions used in the statement, all specialized to real matrices with the standard entrywise operations:

$P_\Omega(A)$ is the $d \times d$ matrix that keeps entry $A_{ij}$ when $(i,j) \in \Omega$ and is $0$ otherwise;
$\langle A, B \rangle = \sum_{i,j} A_{ij} B_{ij}$ is the entrywise (Frobenius) inner product, and $\|A\|_F^2 = \sum_{i,j} A_{ij}^2$ ;
for a $d \times r$ matrix $A$ , its $i$ -th row norm is $\|A_i\| = \sqrt{\sum_j A_{ij}^2}$ ;
$h_i = \max(\|X_i\| - \alpha,\, 0)$ , so that $h_i = 0$ whenever $\|X_i\| \le \alpha$ ;
$R_\alpha(X)$ is the $d \times r$ matrix with entries $\bigl(R_\alpha(X)\bigr)_{ij} = \dfrac{4\, h_i^3}{\|X_i\|}\, X_{ij}$ . Edge case: every quotient in this read-back uses the convention that division by zero yields $0$ ; in particular, if row $i$ of $X$ is the zero row then $\|X_i\| = 0$ and the corresponding quotient terms are $0$ by convention rather than undefined (note that when $\alpha < 0$ , $h_i = -\alpha > 0$ even for a zero row, so the convention is genuinely load-bearing there);
for $d \times r$ matrices $X, V$ , writing $c_i = \dfrac{\sum_j X_{ij} V_{ij}}{\|X_i\|}$ (again $0$ when $\|X_i\| = 0$ ),

H_\alpha(X, V) \;=\; \sum_{i=0}^{d-1} \left[\, 12\, h_i^2\, c_i^2 \;+\; \frac{4\, h_i^3}{\|X_i\|}\,\bigl(\|V_i\|^2 - c_i^2\bigr) \right].

Writing $V = X - U$ , the left-hand side $K$ is, by unfolding its definition, the real number

K \;=\; \underbrace{\Bigl[\, \|P_\Omega(V X^\top + X V^\top)\|_F^2 \;-\; 2\,\bigl\langle P_\Omega(Z Z^\top - X X^\top),\; V V^\top \bigr\rangle \;+\; \lambda\, H_\alpha(X, V) \Bigr]}_{\text{a Hessian-type quadratic form in } V} \;-\; 4\,\bigl\langle G,\; V \bigr\rangle,

where $G$ is the $d \times r$ matrix

G \;=\; 2\, P_\Omega\bigl(X X^\top - Z Z^\top\bigr)\, X \;+\; \lambda\, R_\alpha(X).

The asserted conclusion is the exact identity of real numbers

K \;=\; \|P_\Omega\bigl(V V^\top\bigr)\|_F^2 \;-\; 3\, \|P_\Omega\bigl(X X^\top - U U^\top\bigr)\|_F^2 \;+\; \lambda\, \Bigl( H_\alpha(X, V) \;-\; 4\,\bigl\langle R_\alpha(X),\; V \bigr\rangle \Bigr),

with $V = X - U$ in every occurrence. Note that the right-hand side is written in terms of $X X^\top - U U^\top$ (not $X X^\top - Z Z^\top$ ); under the hypothesis $U U^\top = Z Z^\top$ these coincide, but the statement as written uses $U$ . The hypotheses are jointly satisfiable (e.g. $U = Z$ and $\Omega = \emptyset$ , or $\Omega$ any symmetric set), so the statement is not vacuous; nothing requires $\Omega$ to be nonempty, $Z$ , $X$ , $U$ to be nonzero, $\lambda \ge 0$ , or $\alpha \ge 0$ . The claim is a universally quantified equation only — it asserts no inequality, no minimality, and nothing probabilistic; the sampling, incoherence, and second-order-point definitions present in the surrounding context do not appear in this statement.

Human review

Endorsed by Community (Bot) · Aug 4, 2026
Endorsed by Shuze Chen · Aug 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Decomposition of the auxiliary function KKK (Ge–Jin–Zheng Lemma 7; Chen–Li Lemma 4.7)

Decomposition of the auxiliary function $K$ (Ge–Jin–Zheng Lemma 7; Chen–Li Lemma 4.7)