hankel_det_ne_zero
plain-language theorem explainer
An exponential-sum Hankel matrix built from d distinct real nodes and nonzero amplitudes is nonsingular. CPT and Prony-style identification arguments cite this as the algebraic engine behind nonempty identifiability loci Ω_{d,W}. The proof rewrites the determinant as a squared Vandermonde factor times the product of amplitudes, then invokes nonzero factors from distinct nodes and nonzero amplitudes.
Claim. Let $d \in \mathbb{N}$ and let $E$ be exponential-sum data of order $d$: distinct real nodes $\mu_0,\ldots,\mu_{d-1}$ and amplitudes $B_i \neq 0$. Then the Hankel matrix $H$ with entries $H_{i,j} = \sum_m B_m \mu_m^{i+j}$ satisfies $\det H \neq 0$.
background
This module closes the general $(d,W)$ rank-certification gap for CPT window measurements. The setting is exponential-sum signals $S_k = \sum_i B_i \mu_i^k$ with distinct nodes and nonzero amplitudes; the associated Hankel matrix has entries $H_{i,j} = \sum_m B_m \mu_m^{i+j}$.
ExponentialSumData d packages exactly those hypotheses: a map of $d$ real nodes, a map of amplitudes, a distinctness certificate, and a pointwise nonzero-amplitude certificate. Sibling facts record that this Hankel factors through a Vandermonde matrix on the nodes (via hankel_eq_vandermonde_product / hankel_det) and that the Vandermonde determinant itself is nonzero when nodes are distinct (vandermonde_det_ne_zero, ultimately Mathlib's Matrix.det_vandermonde).
Module strategy: choose distinct real exponents in $(0,1)$; window sums remain exponential sums with distinct nodes because $x \mapsto x^W$ is injective on $(0,1)$ for $W \ge 1$; nonsingularity of the Hankel then witnesses that the identifiability locus $\Omega_{d,W}$ is nonempty.
proof idea
One short algebraic reduction. Rewrite the target determinant via hankel_det, which expresses $\det H$ as $(\det V)^2$ times the product of the amplitudes, where $V$ is the Vandermonde matrix on the nodes. Apply mul_ne_zero to the two factors. The squared Vandermonde factor is nonzero by pow_ne_zero 2 on vandermonde_det_ne_zero applied to the distinct-nodes certificate. The amplitude product is nonzero by Finset.prod_ne_zero_iff and the pointwise amplitudes_nonzero field of the data.
why it matters
This is the algebraic core of general rank certification for CPT: every $(d,W)$ with $d,W \ge 1$ admits a parameter witness whose window-sum Hankel is nonsingular, so $\Omega_{d,W}$ is nonempty (hence Zariski-open dense). The module doc ties the result to the paper gap in Theorem 2.14.
Downstream, identifiability_locus_nonempty is essentially a named wrapper that feeds this nonsingularity into the existence statement for $\Omega_{d,W}$. The export RANK_hankel_det_ne_zero re-exports the same fact for the verification surface. Without a nonzero Hankel determinant, Prony/window identification cannot certify full rank of the measurement map; this lemma supplies that certificate for every exponential-sum witness with distinct nodes and nonzero amplitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.