RANK_hankel_det_ne_zero
plain-language theorem explainer
The Hankel matrix built from an order-d exponential sum with distinct nodes and nonzero amplitudes is nonsingular. CPT and Prony-style identifiability arguments cite this as the algebraic witness that the rank-d model is full rank. The export is a one-line term wrapper around the RankCertification core lemma.
Claim. For every $d \in \mathbb{N}$ and every exponential-sum datum $E$ of order $d$ (distinct nodes, nonzero amplitudes), if $H(E)$ is the associated Hankel matrix then $\det H(E) \neq 0$.
background
This module is the CPT export surface: thin, citation-stable aliases for the fully proved CPT layer (window identifiability, pipeline soundness, optimality, forced factorisation, $\varepsilon$-noise). No new axioms or sorrys live here.
Rank certification treats a finite exponential sum $s_n = \sum_{j=1}^d a_j \lambda_j^n$ with distinct nodes $\lambda_j$ and nonzero amplitudes $a_j$. The Hankel matrix $H(E)$ packs consecutive moments of $s$; classical Prony / Padé theory says full rank of $H$ is equivalent to exact order $d$. In the CPT paper language this nonsingularity witnesses that the identifiability locus $\Omega_{d,W}$ is nonempty for admissible window widths $W$.
The sibling WINDOW_* exports restate identifiability as trivial kernel or full column rank of the window map; the present determinant statement is the concrete algebraic certificate those equivalences rely on.
proof idea
One-line term wrapper: the goal is discharged by applying RankCertification.hankel_det_ne_zero to the same exponential-sum datum $E$. All substance (distinct-node Vandermonde factorisation, nonzero amplitude product, and the resulting Hankel determinant formula) lives in that core lemma; the export only renames it for the paper-facing API.
why it matters
In the CPT formalization this is the rank-side certificate that the identifiability locus $\Omega_{d,W}$ is nonempty whenever an exponential-sum witness exists (the general $(d,W)$ rank-certification claim attached to the export). It sits under the RANK_* family that feeds the window-identifiability theorems (paper Thm. 4.5 / 6.5) and, indirectly, the P→B→A pipeline and forced-factorisation results exported as CPT_PIPELINE_* and CPT_FACTOR_*.
Within Recognition Science the statement is pure linear-algebraic infrastructure for the CPT verification layer rather than a forcing-chain landmark (T5–T8, RCL, eight-tick). It closes the algebraic gap between “there exists a rank-$d$ exponential model” and “the Hankel witness is invertible,” which the window and $\varepsilon$-noise exports then consume. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.