DistinctNodes
plain-language theorem explainer
A predicate asserting that a finite list of real nodes is pairwise distinct (the indexing map is injective). CPT rank-certification proofs cite it as the hypothesis that makes a Vandermonde determinant nonzero. The body is a one-line alias of injectivity; no further argument is needed.
Claim. For $n \in \mathbb{N}$ and $v : \{0,\ldots,n-1\} \to \mathbb{R}$, the distinct-nodes property holds if and only if $v$ is injective: $i \neq j$ implies $v(i) \neq v(j)$.
background
The CPT rank-certification module closes a gap in Theorem 2.14: for every dimension $d \ge 1$ and window $W \ge 1$, the identifiability locus $\Omega_{d,W}$ is nonempty. The strategy is to exhibit a window-sum exponential signal $S_k = \sum_i B_i \mu_i^k$ whose Hankel matrix is nonsingular.
Nonsingularity is obtained by factoring the Hankel matrix through a Vandermonde matrix on the nodes. Mathlib supplies $\det V = \prod_i \prod_{j>i}(v_j - v_i)$, which vanishes precisely when two nodes coincide. The distinct-nodes predicate packages that non-coincidence hypothesis as injectivity of $v : \mathrm{Fin}, n \to \mathbb{R}$.
Downstream, exponential-sum data bundles distinct nodes with nonzero amplitudes; the Vandermonde nonvanishing lemma then feeds Hankel nonvanishing and nonemptiness of $\Omega_{d,W}$.
proof idea
Pure definitional wrapper: the predicate is definitionally equal to Function.Injective v. No tactics, no lemmas. Callers discharge it by exhibiting pairwise inequalities among the chosen real nodes (typically distinct points in $(0,1)$).
why it matters
This is the hypothesis gate for the Vandermonde step in general $(d,W)$ rank certification. It is required by vandermonde_det_ne_zero (and its export RANK_vandermonde_det_ne_zero), and is a field of ExponentialSumData. Those results establish that the window-measurement Hankel matrix can be nonsingular, so the identifiability locus is nonempty (hence Zariski-open dense) for all $(d,W)$. Paper reference: the "$(d,W)$ rank certification" gap in Theorem 2.14. Without a crisp distinct-nodes interface, the Mathlib Vandermonde determinant formula cannot be applied uniformly across window sizes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.