zero_detection_of_identifiable
plain-language theorem explainer
If a finite CPT window measurement matrix is identifiable (injective), then a zero measurement forces the latent vector to vanish. CPT window arguments cite this as the zero-detection half of injectivity. The proof is a short tactic: apply injectivity to the equality of the measured vector with the zero vector, after simplifying the image of zero.
Claim. Let $A$ be a real $m\times n$ matrix and write $M_A$ for the linear measurement map it induces. If $M_A$ is injective and $x\in\mathbb{R}^n$ satisfies $M_A(x)=0$, then $x=0$.
background
This module is the matrix-level core of CPT window identifiability: injective reconstruction from finite window measurements, equivalence with trivial kernel, a full-column-rank predicate defined as injectivity, and zero-detection under that hypothesis. The generic/nondegenerate layer is kept separate as an explicit nonvanishing-minor hypothesis bundle so claim strength stays visible.
Here vectors are coordinate maps Vec n := n → ℝ. Identifiability of a window matrix $A$ means the induced linear measurement map is injective. That is exactly the reconstruction property used downstream: distinct latent states cannot produce the same finite window of observations.
Zero-detection is the special case of injectivity at the origin. It is the form most often needed when a residual or difference signal is observed to vanish and one wants to conclude the latent difference is zero.
proof idea
Introduce the hypothesis $M_A(x)=0$. Apply the injectivity assumption on $A$ to the pair $x$ and $0$. A one-line calculation equates $M_A(x)$ with $0$ by the hypothesis, then rewrites $0$ as $M_A(0)$ by linearity (simp). Injectivity therefore yields $x=0$. No external lemmas beyond the definition of identifiability and basic linear-map simplification are required.
why it matters
Zero-detection is the operational reading of window injectivity: a null CPT window residual forces a null latent state. The export WINDOW_zero_detection_of_identifiable re-packages this statement for the CPT verification surface, so downstream window uniqueness and reconstruction arguments can cite a single named fact rather than unfold injectivity by hand.
In the module hierarchy it sits beside the equivalences identifiable ↔ trivial kernel ↔ full column rank, and below the nonvanishing-minor hypothesis that discharges generic identifiability. It does not itself touch the Recognition forcing chain (T0–T8) or the J-cost law; it is pure linear-algebra scaffolding for the CPT window layer that those physical claims eventually rely on for measurement uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.