hankel_det
plain-language theorem explainer
For exponential-sum data with d nodes and amplitudes, the Hankel matrix determinant equals the square of the Vandermonde determinant on the nodes times the product of the amplitudes. Anyone proving nonsingularity of window Hankels in CPT rank certification cites this identity. The proof is a short algebraic rewrite: factor through the Vandermonde product, apply det-multiplicativity and det of transpose/diagonal, then ring.
Claim. Let $d\in\mathbb{N}$ and let $E$ be exponential-sum data of order $d$: nodes $\mu:Fin\,d\to\mathbb{R}$ that are pairwise distinct and amplitudes $B:Fin\,d\to\mathbb{R}$. Write $H$ for the Hankel matrix $H_{i,j}=\sum_m B_m\,\mu_m^{i+j}$ and $V$ for the Vandermonde matrix on the nodes. Then $\det(H)=\det(V)^2\cdot\prod_i B_i$.
background
This module closes the general $(d,W)$ rank-certification gap for CPT window measurements. The target theorem is that for every $d\ge 1$ and $W\ge 1$ there is a parameter witness at which the window-measurement Hankel is nonsingular, so the identifiability locus $\Omega_{d,W}$ is nonempty (hence Zariski-open dense). Paper reference: the $(d,W)$ rank certification gap in Theorem 2.14.
The local objects are exponential-sum data: a map of nodes $\mu_i\in\mathbb{R}$ together with amplitudes $B_i$, with the nodes pairwise distinct and every amplitude nonzero. The associated Hankel is $H_{i,j}=\sum_m B_m,\mu_m^{i+j}$, the moment matrix of the sequence $S_k=\sum_i B_i\mu_i^k$. A sibling lemma records the classical factorization of this Hankel through a Vandermonde matrix on the nodes (and a diagonal of amplitudes).
The strategy in the module doc is: pick $d$ distinct real exponents in $(0,1)$; the window sums remain an exponential sum with distinct nodes (since $x\mapsto x^W$ is injective on $(0,1)$); the Hankel then factors through a Vandermonde with distinct entries and is nonsingular via Mathlib's Vandermonde determinant.
proof idea
One short term-mode calculation. Rewrite the Hankel via the sibling identity hankel_eq_vandermonde_product, which expresses $H$ as a product of a Vandermonde, a diagonal of amplitudes, and a transposed Vandermonde (up to order). Apply Matrix.det_mul twice, then Matrix.det_transpose (so the two Vandermonde factors contribute the same determinant) and Matrix.det_diagonal (so the middle factor contributes $\prod_i B_i$). Finish by ring to rearrange into $\det(V)^2\cdot\prod_i B_i$.
why it matters
This identity is the algebraic engine behind nonsingularity. The immediate parent is hankel_det_ne_zero, which rewrites along this equality and splits into two nonzero factors: the squared Vandermonde determinant (nonzero because the nodes are distinct) and the product of amplitudes (nonzero by the data hypothesis). That nonsingularity witness is what populates $\Omega_{d,W}$ and discharges the general $(d,W)$ rank-certification gap stated in the module doc for Theorem 2.14.
In the broader Recognition verification stack, window Hankels certify that CPT measurement maps separate exponential-sum signals of order $d$. Without an explicit determinant formula, density of the identifiability locus would remain a scaffolding claim rather than a proved existence statement for every $(d,W)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.