IndisputableMonolith.Verification.CPT.WindowIdentifiability
Formalizes window-matrix identifiability for CPT: a linear measurement map is identifiable iff it has trivial kernel iff it has full column rank. Supplies the classical iff chain, zero-detection, and generic identifiability under a nonvanishing-minor hypothesis. Cited by WINDOW_* exports (paper Thm. 4.5/6.5), the P→B→A pipeline, and general (d,W) rank certification.
claimFor the linear measurement map $M$ induced by a window matrix, the following are equivalent: (i) $M$ is identifiable; (ii) $\ker M=\{0\}$; (iii) $M$ has full column rank. Identifiability implies zero-detection. Under a nonvanishing-minor hypothesis, identifiability holds generically on the parameter space.
background
CPT verification asks when a finite observation window uniquely recovers the underlying signal or parameter. This module builds on CPT Core (decision tags, procedure utilities, class-restricted domination, lightweight CPM A/B/C wrappers) and specializes that interface to the linear window setting.
The central object is the linear measurement map induced by the window matrix: a map from coefficient (or state) space into the observation space. Identifiability means distinct inputs yield distinct observations. Trivial kernel and full column rank are the standard rank-nullity restatements of that property. A nonvanishing-minor hypothesis packages the open condition that some maximal minor is nonzero, forcing full rank on a Zariski-open locus.
proof idea
Definition-and-equivalence package, not a single deep theorem. It introduces the measurement map and the three predicates (identifiable, trivial kernel, full column rank), then proves the classical equivalences by rank-nullity. Zero-detection is the immediate corollary that a zero observation forces a zero input. Generic identifiability is a one-step discharge: assume a nonvanishing maximal minor, conclude full column rank, hence identifiability. No explicit inverse is constructed.
why it matters in Recognition Science
Exports re-exports this material as the WINDOW_* citation surface, mapped to paper Theorems 4.5 and 6.5 (window identifiability family). Pipeline imports it into the certified P→B→A composition (projection/neutrality, coercivity conversion, aggregation/decision). RankCertification uses the same linear-algebra base to close the general (d,W) gap: for every d,W ≥ 1 there is a parameter witness at which the window-measurement Hankel matrix has nonzero determinant, so the identifiability locus Ω_{d,W} is nonempty and therefore Zariski-open dense. Without the iff chain and the minor-hypothesis interface, those density and pipeline results would lack a local foundation.
scope and limits
- Does not construct concrete window or Hankel matrices for specific (d,W).
- Does not prove minors are nonvanishing; that is hypothesized or deferred to RankCertification.
- Does not treat nonlinear or noisy measurement models.
- Does not run the P→B→A pipeline or define WINDOW_* export aliases.
- Does not assert density of the identifiability locus without an external rank witness.
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