Papers With

← All papers
First page of One Extra Dimension Suffices for the Complete-Graph Squared-Stress

One Extra Dimension Suffices for the Complete-Graph Squared-Stress

Lilin Yan, Hongwei Zhao

math.NA Oct 5, 2026 · v1
formalization analysis
Read PDF arXiv abstract Code
TL;DR
The main theorem on second-order stationary points of the squared-stress objective is formalized in Lean 4, starting from real directional derivatives, with a kernel check and an axiom audit.
Abstract
Let all pairwise distances of an arbitrary configuration of points in $\mathbb{R}^{\ell}$ be known exactly. We prove that every second-order stationary point of the complete-graph squared-stress objective over configurations in $\mathbb{R}^{k}$ has zero residual whenever $k > \ell$. The result holds for every number of points, without a genericity assumption, and allows repeated points and degenerate ground-truth configurations. It resolves the one-extra-dimension conjecture for complete, uniformly weighted data. The proof combines positivity of the residual stress, polar normalization of the candidate configuration, a row-wise rank-nullity argument, and propagation of zero curvature through the full Hessian. The theorem, including the passage from derivatives of the original quartic objective to its matrix formulation, has been formalized in Lean 4. The accompanying verification records include a kernel check with zero trust level and a transitive axiom audit.
Problem

The squared-stress (s-stress) objective for recovering point configurations from exact complete pairwise distances can have spurious local minima in the ground-truth dimension. Criscitiello et al. conjectured that optimizing in one extra dimension (k = ℓ+1) removes all non-global second-order stationary points. Only partial results were known.

Approach

The proof shows that the stress matrix is positive semidefinite at first-order points. It then polar-normalizes the candidate configuration and applies a row-wise rank-nullity argument at each row attaining the maximal diagonal stress. Zero curvature is propagated through the full Hessian to force off-diagonal stresses to vanish, which yields a contradiction. The whole argument, including the derivation of the gradient and Hessian from the quartic objective, is formalized in Lean 4. Exact rational-arithmetic Python scripts check the formulas and control examples.

Results

Every second-order stationary point has zero residual whenever k > ℓ, for any number of points and with no genericity assumptions, which resolves the one-extra-dimension conjecture for complete, uniformly weighted data. The Lean theorem SStress.mainStatement_proved is verified, together with corollaries giving exact distances and global minimality. Control examples show the strict dimension inequality is necessary and that positive semidefinite diagonal Hessian blocks alone do not suffice.