measurementLinear
plain-language theorem explainer
The window matrix A is promoted to the ℝ-linear map sending coordinate vectors on the source index set to coordinate vectors on the measurement index set. CPT window arguments cite this as the measurement operator whose injectivity is identifiability. The body is the standard Mathlib conversion Matrix.toLin'.
Claim. Given a real matrix $A$ with rows indexed by a finite measurement set $m$ and columns by a finite source set $n$, write $\mathrm{measurementLinear}(A)$ for the unique $\mathbb{R}$-linear map $V_n \to V_m$ acting by left-multiplication with $A$, where $V_\iota := \iota \to \mathbb{R}$.
background
The module CPT.WindowIdentifiability packages the matrix-level core of CPT window arguments: injective reconstruction from finite window measurements, equivalence with trivial kernel, a full-column-rank predicate defined as injectivity, and zero-detection under identifiability. A named hypothesis bundle NonvanishingMinorHypothesis keeps the generic/nondegenerate layer explicit.
Here Vec is the in-module abbreviation $\iota \to \mathbb{R}$ for real coordinate functions on a finite index type (with Fintype and DecidableEq on the column index). Upstream, Measurement.RSNative.Core supplies the discrete Window structure (start tick and length in ticks) that motivates treating finite windows as matrix measurements; the linear algebra is deliberately kept matrix-level so that injectivity statements stay elementary.
The conversion Matrix.toLin' is Mathlib's standard bridge from a matrix to the corresponding linear map on function spaces, so the measurement operator is exactly left action by $A$.
proof idea
One-line definitional wrapper: the body is Matrix.toLin' A, Mathlib's canonical linear map associated to a matrix acting on coordinate vectors. No further proof obligations; noncomputable only because the ambient linear-map API is marked that way.
why it matters
Every identifiability predicate in the module is stated in terms of this map. Identifiable and FullColumnRank are both Function.Injective of measurementLinear A; TrivialKernel is ker(measurementLinear A) = ⊥. The equivalence identifiable_iff_trivialKernel rewrites through LinearMap.ker_eq_bot applied to this map, and zero_detection_of_identifiable is the direct consequence that an identifiable window sending x to 0 forces x = 0.
In the broader Recognition verification stack this is the linear skeleton under CPT window reconstruction: finite tick windows yield a matrix of linear functionals, and unique recovery of the source vector is injectivity of that map. It does not itself invoke the forcing chain (T0–T8), RCL, or the phi-ladder; it supplies the linear-algebra interface those higher arguments reduce to when they talk about window measurements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.