Pith. sign in
module module moderate

IndisputableMonolith.Verification.CPT.RankCertification

show as:
view Lean formalization →

Rank-certification layer for CPT window identifiability: distinct exponential nodes make the associated Hankel matrix full rank via a Vandermonde factorization. Analysts cite it to justify that finite window measurements separate distinct node sets. The argument is classical linear algebra (Vandermonde determinant nonzero, Hankel as a product, hence det nonzero) plus a nonempty identifiability locus.

claimIf the node set is pairwise distinct, the Hankel matrix built from exponential-sum window data factors through a Vandermonde matrix and therefore has nonzero determinant (full column rank). Consequently the identifiability locus of distinct-node configurations is nonempty.

background

CPT verification sits on reusable Core interfaces (decision tags, resolved sets, class-restricted domination) and on Window Identifiability, which equates injective reconstruction from finite window measurements with trivial kernel of the measurement map and with a full-column-rank predicate.

This module supplies the concrete rank engine behind that predicate. Nodes are treated as distinct exponential parameters. Window data are packaged as exponential-sum samples; the associated Hankel matrix is the natural moment matrix of those samples. Classical Vandermonde theory then controls its determinant.

The local goal is purely algebraic: certify that distinctness of nodes forces the Hankel determinant away from zero, so the measurement map is injective on that locus.

proof idea

Structure is standard Hankel–Vandermonde algebra, not a single deep lemma. Distinct-node hypotheses feed a nonzero Vandermonde determinant. The Hankel matrix of the exponential-sum data is identified with a Vandermonde product factorization. Nonvanishing of the factors yields nonzero Hankel determinant, hence full column rank. A final existence statement records that the distinct-node identifiability locus is nonempty. Supporting definitions package the exponential-sum data and the Hankel construction used throughout.

why it matters in Recognition Science

Window identifiability (paper Thms. 4.5 / 6.5, exported as WINDOW_*) needs a concrete full-rank certificate; without it the measurement map could collapse distinct node configurations. This module closes that linear-algebra gap and is re-exported through the CPT Export surface for the P→B→A pipeline composition.

In the broader Recognition verification stack it is the place where “distinct nodes” becomes a checkable rank condition rather than an informal modeling assumption. Downstream citation should go through the export aliases once the window theorems invoke these rank facts.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)