An algebraic proof of Colombo's difference-power determinant conjecture
Kun Li, Li Tie, Peng Wang, Zihan Liu
cs.LG
Aug 28, 2026 · v1
math.RA
TL;DR
The odd-exponent nonsingularity proof was formalized and kernel-checked in Lean 4 with Mathlib, and an appendix maps paper results to Lean theorems.
Abstract
Let $n\ge2$ be even, let $λ=(λ_1,\ldots,λ_n)\in\mathbb{R}^n$ have pairwise distinct coordinates, and define the difference-power matrix \[ A_d(λ) := \bigl[(λ_r-λ_s)^d\bigr]_{r,s=1}^n, \qquad d\in\mathbb{N}. \] In 1928, Colombo proved that $\det A_{n-1}(λ)\ne0$—and hence $\det A_{n-1}(λ)>0$—and that $\operatorname{rank} A_d(λ)=d+1$ for $0\le d<n-1$. He conjectured that \[ \det A_d(λ)\ne0 \qquad\text{for every } d\ge n-1. \] For even $d$, the conjectured nonsingularity follows from previously published results on distance-power matrices. The remaining open cases were therefore the supercritical odd exponents $d\ge n+1$. We prove nonsingularity for all these odd exponents, thereby completing Colombo's conjecture. Consequently, \[ \operatorname{rank} A_d(λ)=\min\{n,d+1\} \qquad(d\in\mathbb{N}). \] Our proof converts a hypothetical kernel vector into a real binary form having more projective real linear factors, counted with multiplicity, than its real Waring length permits.
Problem
Colombo conjectured in 1928 that the difference-power matrix [(λ_r−λ_s)^d] is nonsingular for even n, pairwise distinct real nodes, and every d ≥ n−1. The even-d cases already follow from known results on distance-power matrices. The supercritical odd exponents d ≥ n+1 remained open.
Approach
The proof assumes a nonzero kernel vector and uses it to build a real binary form F as a combination of d-th powers of linear forms. Apolarity shows that F vanishes at every node, so the product of the n distinct linear factors divides F. The remaining cofactor has odd degree and therefore contributes one more real linear factor. This contradicts a theorem bounding the number of real linear factors by the real Waring length, which is at most n. The odd-exponent argument was formalized and kernel-checked in Lean 4 with Mathlib.
Results
Nonsingularity holds for all odd d ≥ n+1, which completes Colombo's conjecture. It follows that rank A_d = min{n, d+1}, and the sign of the determinant is determined. A Lean formalization independently verifies the odd branch and Colombo's threshold result.
