hankelMatrix
plain-language theorem explainer
Defines the d×d real Hankel matrix of an exponential sum Σ B_m μ_m^k by H_{i,j} = Σ_m B_m μ_m^{i+j}. Anyone proving nonsingularity of window-measurement Hankels in CPT rank certification cites this object. The body is a direct Matrix.of sum over amplitudes times node powers.
Claim. Given dimension $d$ and exponential-sum data consisting of nodes $\mu_m \in \mathbb{R}$ and amplitudes $B_m \in \mathbb{R}$ (with distinct nodes and nonzero amplitudes), the associated Hankel matrix is the $d \times d$ real matrix with entries $H_{i,j} = \sum_{m=0}^{d-1} B_m \, \mu_m^{i+j}$.
background
The 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-sum Hankel nonsingular, so the identifiability locus $\Omega_{d,W}$ is nonempty (hence Zariski-open dense). Paper reference: the $(d,W)$ gap in Theorem 2.14.
Exponential-sum data packages $d$ real nodes $\mu_m$ and amplitudes $B_m$ with the standing hypotheses that the nodes are pairwise distinct and every amplitude is nonzero. The signal is $S_k = \sum_m B_m \mu_m^k$. The Hankel matrix of such a signal is the classical moment matrix with entries indexed by power sums $i+j$.
Downstream arguments factor this Hankel through a Vandermonde matrix on the nodes: $H = V^\top \mathrm{diag}(B) V$. Distinct nodes make $\det V \ne 0$ (Mathlib Matrix.det_vandermonde), and nonzero amplitudes keep the diagonal product nonzero, so $\det H \ne 0$.
proof idea
Definition only: no proof obligations. The matrix is built by Matrix.of with entry $(i,j)$ equal to the finite sum over $m : \mathrm{Fin}, d$ of amplitude$_m$ times node$_m$ raised to $i.val + j.val$. That is exactly the classical Hankel of the exponential sum. Later lemmas (hankel_eq_vandermonde_product, hankel_det) expand this definition and rewrite it as the Vandermonde sandwich.
why it matters
This is the concrete matrix whose determinant witnesses rank certification. Immediate consumers: hankel_eq_vandermonde_product (the factorization $H = V^\top \mathrm{diag}(B) V$), hankel_det ($\det H = (\det V)^2 \prod B_i$), and hankel_det_ne_zero. Those feed identifiability_locus_nonempty and the export theorems RANK_hankel_det_ne_zero and RANK_identifiability_locus_nonempty, which state that for any $d,W \ge 1$ an exponential-sum witness makes the Hankel nonsingular, so $\Omega_{d,W}$ is nonempty.
In the CPT verification stack this closes the general-rank gap left open by window-identifiability arguments: once a single nonsingular Hankel exists, the identifiability locus is Zariski-open dense. The construction is pure linear algebra on exponential sums; it does not itself invoke the Recognition forcing chain (T5–T8) or the RCL, but it underwrites the measurement-side uniqueness claims those layers rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.