cs.LGAug 28, 2026
SaveAn algebraic proof of Colombo's difference-power determinant conjecture
Abstract
Let be even, let have pairwise distinct coordinates, and define the difference-power matrix
In 1928, Colombo proved that ---and hence ---and that for . He conjectured that
For even , the conjectured nonsingularity follows from previously published results on distance-power matrices. The remaining open cases were therefore the supercritical odd exponents . We prove nonsingularity for all these odd exponents, thereby completing Colombo's conjecture. Consequently,
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.
Figures & tables
Appendix figures & tables1 asset
Supplementary material from the paper’s appendix.
Appendix
| Paper result | Lean file | Lean theorem | Formal role |
|---|---|---|---|
| Threshold exponent | OddBranch | threshold_nonsingular | Independently verifies Colombo’s threshold result. |
| Odd root-count bound | OddBranch | projectiveRootCount_powerSum_le_support | Formalizes the Sylvester–Reznick support bound. |
| All odd exponents | OddBranch | odd_nonsingular | Matches the argument of Section 3 . |
Table 1. Correspondence between paper results and Lean proof terms.