TrivialKernel
plain-language theorem explainer
Trivial kernel means the linear map induced by a finite window measurement matrix has kernel equal only to zero. CPT reconstruction arguments cite it as the kernel form of window identifiability. It is a one-line Prop abbreviation equating that kernel to the bottom subspace.
Claim. For a real $m \times n$ matrix $A$, the trivial-kernel property holds when $\ker(L_A)=\{0\}$, where $L_A:\mathbb{R}^n\to\mathbb{R}^m$ is the linear map induced by $A$.
background
The CPT window-identifiability module treats finite-data reconstruction as a linear-algebra problem on window matrices. A window matrix $A$ induces a measurement map $L_A:\mathbb{R}^n\to\mathbb{R}^m$ via the standard matrix-to-linear-map construction; that map is the module's measurementLinear.
Identifiability is injectivity of that map: distinct source vectors produce distinct window observations. In finite dimensions, injectivity is equivalent to a trivial kernel and to full column rank (here defined as injectivity of the same map). The module keeps a separate named nonvanishing-minor hypothesis for the generic/nondegenerate layer so claim strength stays explicit.
Upstream, the measurement map is exactly Matrix.toLin' A on the finite real vector spaces used for window data. Downstream equivalences then move freely among injectivity, trivial kernel, and full column rank.
proof idea
Definitional, not a proof. The body is the single Prop equation LinearMap.ker (measurementLinear A) = ⊥, i.e. the kernel of the matrix-induced linear map equals the zero subspace. No tactics or lemmas are applied at this declaration; later theorems unfold this abbreviation against Mathlib's LinearMap.ker_eq_bot.
why it matters
This is the kernel-side vocabulary for paper-level CPT window theorems. It is used by the local equivalence identifiable_iff_trivialKernel and by the export WINDOW_identifiable_iff_trivialKernel, documented as identifiability ↔ trivial kernel (paper Thm. 6.5). It also feeds trivialKernel_iff_fullColumnRank, closing the triangle with the full-column-rank predicate (paper Thm. 4.5).
In the Recognition verification stack, window identifiability is the finite-measurement gate: if the kernel is nontrivial, distinct ladder or mode configurations can share the same window data, so reconstruction and zero-detection fail. Naming the kernel form separately keeps the linear-algebra content readable next to the injectivity form without changing mathematical strength.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.