Identifiable
plain-language theorem explainer
A real m-by-n window matrix is identifiable when its induced linear measurement map is injective, so distinct source vectors produce distinct window observations. CPT window reconstruction arguments cite this as the matrix-level definition of unique recovery. The body is a one-line Prop alias for injectivity of the map v ↦ A v.
Claim. A matrix $A \in \mathbb{R}^{m \times n}$ is identifiable when the linear map $v \mapsto Av$ (from $\mathbb{R}^n$ to $\mathbb{R}^m$) is injective.
background
The CPT window-identifiability module packages the linear-algebra core used in finite-window reconstruction: injectivity of measurements, equivalence with trivial kernel, a full-column-rank predicate (here identified with injectivity), and zero-detection under that hypothesis. A named nonvanishing-minor bundle keeps the generic/nondegenerate layer explicit.
The measurement map is the linear map induced by the window matrix via Matrix.toLin': it sends a source vector in $\mathbb{R}^n$ to the observed window in $\mathbb{R}^m$. Identifiability is exactly injectivity of that map, so two sources that agree on the window must be equal.
Sibling predicates (trivial kernel, full column rank) are set up to match this definition, so later equivalences are essentially definitional or standard linear-map facts.
proof idea
Definition, not a proved theorem. The Prop is literally Function.Injective applied to the linear measurement map of $A$. No tactics or lemmas are invoked at this site; downstream results unfold this alias and apply kernel or rank facts.
why it matters
This is the matrix-level claim that the CPT window exports re-export as paper-facing statements. Downstream, identifiability is shown equivalent to trivial kernel (export Thm. 6.5) and to full column rank (export Thm. 4.5), and it yields zero-detection: if $Av=0$ and $A$ is identifiable then $v=0$.
In-module, the generic layer closes by assuming a nonvanishing-minor hypothesis and concluding identifiability. The definition therefore anchors the whole verification stack for unique reconstruction from finite CPT windows, without yet asserting that any particular physical window matrix meets the criterion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.