ExponentialSumData
plain-language theorem explainer
Packages d real nodes and amplitudes for an exponential sum Σ B_i μ_i^k, requiring pairwise distinct nodes and nonzero amplitudes. Anyone proving Hankel nonsingularity or nonemptiness of the CPT identifiability locus Ω_{d,W} cites this bundle. It is a pure structure definition: injectivity of the node map plus pointwise nonvanishing of amplitudes, with no proof obligations beyond those fields.
Claim. For $d \in \mathbb{N}$, an exponential-sum datum is a pair of maps $\mu, B : \{0,\ldots,d-1\} \to \mathbb{R}$ such that $\mu$ is injective (pairwise distinct nodes) and $B(i) \neq 0$ for every index $i$.
background
The module closes the general $(d,W)$ rank-certification gap in CPT verification: for every $d \ge 1$ and $W \ge 1$, some parameter witness makes the window-measurement Hankel matrix nonsingular, so the identifiability locus $\Omega_{d,W}$ is nonempty (hence Zariski-open dense). The strategy treats window sums as exponential sums $S_k = \sum_i B_i \mu_i^k$ and factors their Hankel matrix through a Vandermonde matrix.
Distinct-node data means an injective map $v : \mathrm{Fin}, n \to \mathbb{R}$. That injectivity is exactly what Mathlib's Vandermonde determinant formula needs: $\det V = \prod_i \prod_{j>i}(v_j - v_i) \neq 0$ when entries are pairwise distinct. Amplitudes enter as the diagonal factor in the classical factorization $H = V^\top \mathrm{diag}(B) V$.
This structure is the typed carrier for those two hypotheses together, so every subsequent Hankel construction and determinant identity can take a single argument rather than a loose pair of maps plus side conditions.
proof idea
No proof body: a structure declaration. Fields are the node map, the amplitude map, a proof that nodes are injective (the distinct-node predicate), and a proof that every amplitude is nonzero. Downstream lemmas unpack those fields; nothing is proved at this declaration itself.
why it matters
This is the input type for the whole rank-certification pipeline. hankelMatrix builds $H_{i,j} = \sum_m B_m \mu_m^{i+j}$ from it; hankel_eq_vandermonde_product gives $H = V^\top \mathrm{diag}(B) V$; hankel_det yields $\det H = (\det V)^2 \prod B_i$; and hankel_det_ne_zero concludes $\det H \neq 0$ from distinct nodes and nonzero amplitudes.
Exports re-export those facts as RANK_hankel_det_ne_zero and RANK_identifiability_locus_nonempty, the latter stating general $(d,W)$ rank certification: any such witness shows $\Omega_{d,W}$ nonempty. The module doc ties this to the paper gap in Theorem 2.14. In the Recognition verification stack it is the algebraic certificate that window Hankel rank is full for some open set of parameters, not a physical forcing step (T0–T8), but the linear-algebraic backbone of CPT identifiability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.