FullColumnRank
plain-language theorem explainer
Defines full column rank for a real window matrix as injectivity of the induced linear measurement map from source vectors to window observations. CPT reconstruction arguments cite it as the matrix-level rank predicate equivalent to identifiability. The body is a one-line abbreviation of injectivity of that map.
Claim. A real $m \times n$ matrix $A$ has full column rank when the linear map $x \mapsto A x$ (from $\mathbb{R}^n$ to $\mathbb{R}^m$) is injective.
background
The CPT window-identifiability module treats finite window data as a real matrix $A$ and asks when source parameters can be recovered uniquely from the window measurements. The linear measurement map is the standard matrix-induced map $\mathrm{toLin}'(A):\mathbb{R}^n\to\mathbb{R}^m$.
Identifiability is defined as injectivity of that map; trivial kernel is the equivalent kernel condition. This definition packages the same injectivity under the classical name "full column rank," matching the finite-data reconstruction sense used in the paper's window theorems.
Upstream, measurementLinear is exactly that matrix-to-linear-map conversion. The module keeps a separate named hypothesis bundle for nonvanishing maximal minors so generic/nondegenerate rank claims stay explicit rather than hidden.
proof idea
Definitional abbreviation only: full column rank is declared to mean injectivity of the linear measurement map induced by $A$. No tactics or lemmas; the predicate is literally Function.Injective (measurementLinear A).
why it matters
This predicate is the rank side of the paper's identifiability equivalences. Downstream, identifiable_iff_fullColumnRank is definitional (rfl), and the export WINDOW_identifiable_iff_fullColumnRank records Identifiability $\leftrightarrow$ full column rank as paper Thm. 4.5.
It also feeds trivialKernel_iff_fullColumnRank and appears as the sole field of NonvanishingMinorHypothesis, the explicit bridge that assumes a nonvanishing maximal minor and exposes only the resulting full-column-rank/identifiability consequence. In the CPT verification stack it is the shared matrix-level language for unique reconstruction from finite windows, not a dynamical or mass-ladder claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.