WINDOW_zero_detection_of_identifiable
plain-language theorem explainer
If a real matrix is window-identifiable (its linear measurement map is injective), the only vector it sends to zero is the zero vector. CPT formalization users cite this export alias for the zero-detection half of paper Theorems 4.5/6.5. The proof is a one-line re-export of the core window-identifiability zero-detection lemma.
Claim. Let $A$ be an $m\times n$ real matrix that is window-identifiable, meaning the associated linear measurement map is injective. Then for every $v\in\mathbb{R}^n$, if $Av=0$ then $v=0$.
background
The CPT export module is a citation surface: fully proved aliases with no new axioms or sorry. The WINDOW_* family maps to paper Theorems 4.5 and 6.5 (window identifiability).
Window identifiability means the measurement map of a matrix $A$ is injective: distinct inputs yield distinct measurement outputs. An equivalent reading is that the kernel of the measurement is trivial.
The upstream core lemma states that under identifiability, observing zero output forces the input to be zero. This export restates that fact under the WINDOW_* naming convention used by the paper-to-Lean map.
proof idea
One-line term wrapper. It applies the upstream WindowIdentifiability zero-detection lemma to the same matrix, identifiability hypothesis, vector, and exact kernel equation $A v = 0$. No extra algebraic steps are introduced at the export layer.
why it matters
This alias belongs to the WINDOW_* export family for paper Theorems 4.5/6.5. It packages the kernel-triviality consequence of measurement injectivity so downstream citations need not import the internal window-identifiability module.
Sibling exports give the iff forms via trivial kernel and full column rank; nearby CPT_* exports cover the P→B→A pipeline, φ* optimality, and forced factorization (paper §§5–6, Thm. 5.1, Thm. 6.11). The current graph lists no dependents, so the declaration is an export endpoint rather than an intermediate lemma.
In the Recognition verification layer it certifies that identifiable windows detect null signals exactly, which is the clean-signal half of the CPT soundness story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.