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, Vandermonde nondegeneracy, and Hankel determinants built from finite window moments. Supplies the algebraic nonvanishing facts that turn full-column-rank of the measurement map into a concrete, checkable criterion. Cited by anyone closing the WINDOW_* family or the P→B→A pipeline. Argument is classical linear algebra (Vandermonde factorization of Hankel) packaged for the CPT interfaces.

claimFor distinct nodes $z_1,\ldots,z_r$ and exponential-sum window data, the associated Hankel matrix factors through a Vandermonde product; its determinant is nonzero precisely when the nodes are pairwise distinct, so the measurement map has trivial kernel and the identifiability locus is nonempty.

background

CPT verification sits on small reusable interfaces from the core module: decision tags (zero/nonzero/inconclusive), procedure and resolved-set utilities, and class-restricted domination, plus lightweight wrappers around the CPM A/B/C closure theorems.

Window identifiability formalizes the matrix-level core used in CPT window arguments: injective reconstruction from finite window measurements, equivalence with trivial kernel of the measurement map, and equivalence with a full-column-rank predicate (defined as injectivity).

This module supplies the concrete rank certificates those equivalences need. It introduces a distinct-node predicate, exponential-sum window data, the Hankel matrix of moments, and the classical identity that the Hankel factors as a Vandermonde product. Nonvanishing of the Vandermonde (hence Hankel) determinant is the algebraic content of "full column rank" for distinct nodes.

proof idea

The module is a short linear-algebra package, not a single theorem. Distinct-node hypotheses feed a standard Vandermonde determinant nonvanishing lemma. Exponential-sum window data define a Hankel matrix of moments; a factorization identity writes that Hankel as a product involving the Vandermonde. Determinant multiplicativity then lifts node distinctness to Hankel nondegeneracy. The nonempty-identifiability-locus statement assembles these facts into the rank side of the window-identifiability equivalences from the upstream module.

why it matters in Recognition Science

Exports pulls this material into the citation-friendly CPT surface. Downstream doc states that WINDOW_* aliases map to paper Theorems 4.5 / 6.5 (window identifiability family) and CPT_PIPELINE_* to the P→B→A pipeline (§5 / §6 composition), all fully proved with no sorry and no new axiom.

Without certified Hankel/Vandermonde nondegeneracy, full-column-rank remains an abstract injectivity claim. This module closes that gap: distinct nodes imply nonzero Hankel determinant, hence trivial kernel of the measurement map, hence injective reconstruction from finite windows. It is the algebraic hinge between the matrix-level identifiability core and the exported WINDOW_* theorems used in the CPT composition pipeline.

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)