identifiability_locus_nonempty
plain-language theorem explainer
For every d ≥ 1 and window length W ≥ 1, any exponential-sum signal with distinct nodes and nonzero amplitudes has nonsingular Hankel matrix. That certifies nonemptiness of the CPT identifiability locus Ω_{d,W}. The rank-certification export cites it to close the general (d,W) gap in Theorem 2.14. Proof is a one-line application of the Hankel-determinant nonvanishing lemma.
Claim. For all $d \ge 1$, $W \ge 1$, and every exponential-sum datum $E$ of $d$ distinct real nodes $\mu_i$ with nonzero amplitudes $B_i$, the Hankel matrix $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 in the CPT verification stack. The object of study is the window-measurement Hankel matrix of an exponential-sum signal $S_k = \sum_i B_i \mu_i^k$. Identifiability of the underlying nodes from window sums is governed by nonsingularity of that Hankel matrix; the set of good parameters is the locus $\Omega_{d,W}$.
ExponentialSumData d packages $d$ real nodes together with amplitudes, requiring the nodes to be pairwise distinct and every amplitude nonzero. The associated Hankel matrix is $H_{i,j} = \sum_m B_m \mu_m^{i+j}$. Upstream work in the same module factors this Hankel through a Vandermonde product and proves its determinant is nonzero whenever the nodes are distinct and amplitudes are nonzero (via Mathlib's Vandermonde determinant).
The module strategy is existential: choose $d$ distinct exponents in $(0,1)$; for $W \ge 1$ the map $x \mapsto x^W$ stays injective on $(0,1)$, so the window-sum sequence remains an exponential sum with distinct nodes, and the Hankel is nonsingular.
proof idea
One-line term wrapper: apply hankel_det_ne_zero to the given exponential-sum datum $E$. That upstream lemma already encodes the Vandermonde factorization of the Hankel matrix and the nonvanishing of its determinant under distinct nodes and nonzero amplitudes. The hypotheses $d > 0$ and $W > 0$ are present only to match the $\Omega_{d,W}$ interface; they are unused in the term.
why it matters
This is the named witness that $\Omega_{d,W}$ is nonempty for every $d \ge 1$ and $W \ge 1$. Nonemptiness plus the algebraic (polynomial) character of the determinant implies the locus is Zariski-open dense, which is the content needed for general rank certification.
Downstream, RANK_identifiability_locus_nonempty in the CPT Exports module re-exports the result verbatim as the public rank-certification API. The module doc ties it directly to the paper: it resolves the "$(d,W)$ rank certification" gap in Theorem 2.14. Within the broader Recognition verification layer this supplies the missing existence half of window-identifiability for arbitrary window length, so CPT reconstruction arguments no longer need ad-hoc rank checks per $(d,W)$ pair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.