IndisputableMonolith.Verification.CPT.WindowIdentifiability
Defines window-matrix identifiability for CPT: a linear measurement map is identifiable exactly when its kernel is trivial, equivalently when the window Hankel has full column rank. Supplies the iff chain linking those three predicates, a zero-detection corollary, and a generic-identifiability result under a nonvanishing-minor hypothesis. Downstream rank certification and the CPT export surface cite this layer for paper Thm. 4.5 / 6.5.
claimFor a window measurement matrix inducing a linear map $M$, the following are equivalent: (i) $M$ is identifiable; (ii) $\ker M = \{0\}$; (iii) $M$ has full column rank. Under a nonvanishing-minor hypothesis, identifiability holds generically. Identifiability implies zero-signal detection.
background
CPT verification treats finite window observations as linear measurements of an underlying signal class. The core module supplies decision tags (zero/nonzero/inconclusive), procedure utilities, and class-restricted domination; this module specializes that interface to the window matrix.
The central object is the linear measurement map induced by the window matrix (the DOC_COMMENT's "measurementLinear"). Identifiability means distinct signals in the model class produce distinct window observations. Trivial kernel and full column rank are the standard linear-algebra translations of that property for finite-dimensional parameter spaces.
The nonvanishing-minor hypothesis is the algebraic certificate that some maximal minor of the window Hankel is nonzero at a parameter point, which opens the door to Zariski-open density arguments used later in rank certification.
proof idea
The module is a short linear-algebra layer, not a deep proof development. It introduces predicates Identifiable, TrivialKernel, and FullColumnRank on the window measurement map, then proves the three standard equivalences by rewriting through the definitions of kernel and rank. Zero-detection is an immediate corollary: an identifiable map sends only the zero signal to the zero observation. Generic identifiability is a one-step application of the nonvanishing-minor hypothesis to full column rank, hence to identifiability. No heavy tactics; mostly definitional iff chains.
why it matters in Recognition Science
This is the mathematical core of the WINDOW_* family exported for paper Theorems 4.5 and 6.5 (window identifiability). Exports re-exports citation-friendly aliases built on these predicates. RankCertification closes the general $(d,W)$ gap by producing a parameter witness with nonzero Hankel determinant, which discharges the nonvanishing-minor hypothesis and shows the identifiability locus $\Omega_{d,W}$ is nonempty (hence Zariski-open dense) for every $d,W \ge 1$. Pipeline imports the same layer so the $P \to B \to A$ composition can treat window measurements as identifiable inputs before coercivity conversion and aggregation. Without this module, the CPT formalization would lack the linear-algebra bridge from window matrices to certified recovery.
scope and limits
- Does not construct an explicit nonzero minor for arbitrary $(d,W)$; that is RankCertification's job.
- Does not prove measure-theoretic almost-everywhere claims; only algebraic/Zariski genericity under the minor hypothesis.
- Does not address nonlinear or infinite-dimensional measurement models.
- Does not run the full $P \to B \to A$ pipeline; only supplies the identifiability predicates it consumes.
- Does not fix numerical window length or ambient dimension; those remain parameters.
used by (3)
depends on (1)
declarations in this module (11)
-
abbrev
Vec -
def
measurementLinear -
def
Identifiable -
def
TrivialKernel -
def
FullColumnRank -
theorem
identifiable_iff_trivialKernel -
theorem
identifiable_iff_fullColumnRank -
theorem
trivialKernel_iff_fullColumnRank -
theorem
zero_detection_of_identifiable -
structure
NonvanishingMinorHypothesis -
theorem
generic_identifiability_assuming_nonvanishing_minor