发表机构
Northwestern Polytechnical University（西北工业大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明在完全图平方应力目标下，当嵌入维度高于真实维度时，所有二阶平稳点残差为零，解决了均匀加权数据的一额外维度猜想，并通过Lean 4完成形式化验证。
AI 中文摘要
设 $\mathbb{R}^{\ell}$ 中任意点配置的所有两两距离均已知。我们证明，当 $k > \ell$ 时，$\mathbb{R}^{k}$ 中配置的完全图平方应力目标函数的每个二阶平稳点的残差均为零。该结果适用于任意数量的点，无需一般性假设，并允许重复点和退化的真实配置。它解决了完全、均匀加权数据的一额外维度猜想。证明结合了残差应力的正性、候选配置的极坐标归一化、逐行秩零化论证以及通过完整 Hessian 矩阵传播的零曲率。该定理（包括从原始四次目标函数的导数到其矩阵表述的过渡）已在 Lean 4 中形式化。随附的验证记录包括零信任级别的内核检查和传递公理审计。
英文摘要
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.
Comments9 pages. Lean 4 formalization and exact arithmetic checks included as ancillary files
