vandermonde_det_ne_zero
plain-language theorem explainer
For any finite list of pairwise distinct real nodes, the associated Vandermonde matrix has nonzero determinant. CPT rank-certification cites this to guarantee that exponential-sum Hankel matrices are nonsingular once nodes are distinct. The proof is a short term argument: expand via Mathlib's product formula for the Vandermonde determinant and use injectivity of the node map to kill every factor.
Claim. Let $n\in\mathbb{N}$ and let $v:\{0,\ldots,n-1\}\to\mathbb{R}$ be injective (pairwise distinct nodes). Then $\det V(v)\neq 0$, where $V(v)$ is the Vandermonde matrix with entries $V(v)_{ij}=v(i)^{j}$.
background
This module closes the general $(d,W)$ rank-certification gap for CPT window measurements: for every $d\ge 1$ and $W\ge 1$, some parameter witness makes the window Hankel matrix nonsingular, so the identifiability locus $\Omega_{d,W}$ is nonempty (hence Zariski-open dense). The strategy is classical exponential-sum structure: choose $d$ distinct real exponents in $(0,1)$, form window sums $S_k=\sum_i B_i\mu_i^k$, and factor the Hankel matrix through a Vandermonde matrix on those nodes.
DistinctNodes is simply injectivity of the node map $v:\mathrm{Fin},n\to\mathbb{R}$. Mathlib supplies the product formula $\det V(v)=\prod_i\prod_{j>i}(v_j-v_i)$. Nonvanishing of that product is exactly the algebraic content needed before amplitudes enter the Hankel factorization.
proof idea
Rewrite the goal with Mathlib's det_vandermonde, replacing the determinant by the double product $\prod_i\prod_{j\in I_{>i}}(v_j-v_i)$. Apply Finset.prod_ne_zero_iff twice to reduce to a single factor $v_j-v_i$ with $j>i$. Injectivity of $v$ (the DistinctNodes hypothesis) gives $v_j\neq v_i$, so the difference is nonzero after a sub_ne_zero/Ne.symm cleanup. No induction or case split is required.
why it matters
This is the pure linear-algebra step under the Hankel nonsingularity theorem hankel_det_ne_zero, which multiplies a squared Vandermonde determinant by a product of nonzero amplitudes. That Hankel result is the witness that $\Omega_{d,W}$ is nonempty for all $(d,W)$, resolving the rank-certification gap named in Theorem 2.14 of the paper (module doc). The export RANK_vandermonde_det_ne_zero re-exports the same fact at the CPT verification boundary. Within Recognition Science verification, it is scaffolding for identifiability of window measurements, not a forcing-chain (T0–T8) landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.