RANK_identifiability_locus_nonempty
plain-language theorem explainer
For every order d≥1 and window width W≥1, any exponential-sum witness yields a nonsingular Hankel matrix, so the CPT identifiability locus Ω_{d,W} is nonempty. Citation target for rank-certification claims in the CPT export surface. One-line re-export of the RankCertification nonemptiness theorem.
Claim. For all integers $d\ge 1$ and $W\ge 1$, and for every exponential-sum datum $E$ of order $d$, the Hankel matrix $H(E)$ associated to $E$ satisfies $\det H(E)\ne 0$. Equivalently, the identifiability locus $\Omega_{d,W}$ is nonempty.
background
This module is the CPT export surface: thin, citation-friendly aliases for fully proved results in the CPT formalization layer (window identifiability, pipeline soundness, optimality, forced factorization, and the ε-noise layer). No new axioms or sorries appear here.
Rank certification sits under the window-identifiability family (paper Thm. 4.5 / 6.5). An exponential-sum datum of order $d$ packages the discrete moments that fill a Hankel matrix $H(E)$. Full column rank of that Hankel (equivalently $\det H(E)\ne 0$ in the square case used here) is the algebraic certificate that the observation window of width $W$ separates the $d$-parameter model: the kernel is trivial and the state is identifiable.
Sibling exports state the equivalent formulations: identifiable iff trivial kernel, identifiable iff full column rank, and zero-detection from identifiability. The present theorem only asserts nonemptiness of the locus where those equivalences can fire.
proof idea
Pure one-line term wrapper. It applies RankCertification.identifiability_locus_nonempty at the same $(d,W)$ and the same exponential-sum witness $E$, forwarding the positivity hypotheses $d>0$ and $W>0$. No local algebra is redone on the export surface.
why it matters
Closes the existence half of general-$(d,W)$ rank certification on the CPT citation surface: without a nonempty identifiability locus, the WINDOW_* equivalences (identifiable iff trivial kernel / full column rank) and the downstream pipeline soundness / forced-factorization theorems have no concrete witness to attach to. It is the rank-side counterpart to the WINDOW and CPT_PIPELINE exports listed in the module map (paper §§4–6).
In the broader Recognition stack this is verification infrastructure rather than a forcing-chain step (T5–T8). It certifies that the discrete exponential-sum / Hankel route used to read off model order is algebraically non-vacuous for every positive order and window, so later ε-noise and optimality layers can quantify around a genuine full-rank base point. used_by is currently empty: the declaration is an export endpoint meant for external citation, not an internal lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.