Colombo1928

中文说明

A complete Lean 4 formalization of the nonsingularity of Colombo's 1928 difference-power determinant.

For an even integer n ≥ 2, pairwise distinct real nodes λ : Fin n → ℝ, and every integer exponent d ≥ n - 1, this project proves

det [ (λᵢ - λⱼ)^d ] ≠ 0.

The top-level theorem is Colombo1928.colombo1928 in Colombo1928/Main.lean:

theorem colombo1928 {n d : ℕ} (h_n : 2 ≤ n) (h_n_even : Even n)
    (nodes : Fin n → ℝ) (h_nodes : Function.Injective nodes)
    (h_range : n - 1 ≤ d) :
    (diffPowMatrix nodes d).det ≠ 0

The formalization covers the threshold case d = n - 1, all larger odd exponents, and all even exponents in the stated range.

Installation

• Lean 4.32.1
• mathlib v4.32.1

The exact Lean toolchain and mathlib revision are pinned by lean-toolchain and lake-manifest.json.

Install elan, clone this repository, and enter the repository directory.

Usage and verification

Build the complete formalization and audit the top-level theorem:

lake build
lake env lean Audit.lean

The audit should report:

'Colombo1928.colombo1928' depends on axioms: [propext, Classical.choice, Quot.sound]

These are standard Lean/mathlib foundations. The project contains no custom axiom declaration and no sorry or admit placeholder.

Proof structure

File	Role
Basic.lean	Difference-power matrices and parity/transposition identities
Vandermonde.lean	Linear independence of shifted pure-power vectors
Apolar.lean	Normalized apolar pairing
ProjectiveRoots.lean	Kernel polynomials, node divisibility, and projective real-root counts
SylvesterReznick.lean	Projective real-root bound for sums of real powers
OddBranch.lean	Threshold and odd-exponent branches
AlternatingKernel.lean	Strict alternation of kernels of odd-order skew difference-power matrices
EvenDistance.lean	Polar-derivative bridge and the even-exponent branch
Main.lean	Assembly of all branches into the final theorem
Tests.lean	Module and concrete-parameter regression tests

Scope and status

This repository publishes the Lean source and its machine-checkable theorem. It does not claim that Lean kernel verification by itself establishes external peer review or historical priority.

License

Licensed under the Apache License 2.0.