Existence of an aligned exact factor: $UU^\top=ZZ^\top$ with $X^\top U\succeq 0$ (Chen–Li §4.2.1)

Read-back: MatrixCompletion.NoSpuriousMin.alignment_exists

For every pair of natural numbers $d$ and $r$ (both implicit, including the degenerate cases $d = 0$ and $r = 0$), and for every pair of real matrices $Z, X \in \mathbb{R}^{d \times r}$ — with no hypotheses whatsoever placed on $Z$, $X$, $d$, or $r$ — the statement asserts the existence of a matrix $U \in \mathbb{R}^{d \times r}$ (mere existence, $\exists$, not unique existence) satisfying both of the following:

• $U U^{\mathsf T} = Z Z^{\mathsf T}$, an equality of $d \times d$ matrices;
• the $r \times r$ matrix $X^{\mathsf T} U$ is positive semidefinite, in the sense that (i) $X^{\mathsf T} U$ equals its own transpose (symmetry is part of the definition, not merely assumed), and (ii) for every vector $x \in \mathbb{R}^{r}$, the quadratic form is nonnegative: $x^{\mathsf T} (X^{\mathsf T} U)\, x \ge 0$ (a non-strict inequality, quantified over all $x$, including $x = 0$).

Although the statement lives in a namespace whose surrounding context defines matrix-completion notions (sampling sets, incoherence, objectives, critical points, etc.), the theorem itself uses none of those definitions: it quantifies over completely arbitrary $Z$ and $X$ and mentions only matrix multiplication, transpose, and positive semidefiniteness. When $d = 0$ or $r = 0$ the claim is trivially satisfiable (all matrices involved are empty, $U U^{\mathsf T} = Z Z^{\mathsf T}$ holds vacuously entry-wise, and the quadratic-form condition is vacuous or reduces to $0 \ge 0$). The proof body in the file is a sorry placeholder, i.e., the statement is asserted without proof.