identifiable_iff_trivialKernel
plain-language theorem explainer
For a real window matrix A, injectivity of the induced measurement map is equivalent to that map having trivial kernel. CPT window reconstruction arguments cite this to switch freely between the two formulations of identifiability. The proof is a one-line rewrite via the standard linear-algebra fact that a linear map is injective iff its kernel is bottom.
Claim. For any real matrix $A$ of size $m \times n$, the induced measurement map is injective if and only if its kernel is $\{0\}$.
background
The CPT Window Identifiability module packages the matrix-level core of finite-window reconstruction: injective recovery from window measurements, the trivial-kernel formulation, a full-column-rank predicate (defined here as injectivity), and zero-detection under identifiability.
The measurement map is the linear map $\mathbb{R}^n \to \mathbb{R}^m$ induced by $A$ via Matrix.toLin'. Window identifiability means that map is injective. The trivial-kernel formulation asserts that its kernel equals the zero subspace. Both are pure linear-algebra predicates on the same map; no Recognition-specific constants enter at this layer.
Upstream, the only substantive dependency is that measurement map construction. The equivalence itself is the classical fact that a linear map between vector spaces is injective precisely when its kernel is trivial.
proof idea
One-line term proof. Unfold both sides of the biconditional to Function.Injective (measurementLinear A) and LinearMap.ker (measurementLinear A) = ⊥, then apply the Mathlib identity LinearMap.ker_eq_bot (in the reverse direction) and finish by simpa. No case splits and no matrix arithmetic.
why it matters
This is the bridge between the two standard formulations of window identifiability in the CPT verification stack. The export WINDOW_identifiable_iff_trivialKernel re-exports it as paper Theorem 6.5. The sibling trivialKernel_iff_fullColumnRank routes through this lemma to connect trivial kernel to the full-column-rank predicate, closing the three-way equivalence (identifiable / trivial kernel / full column rank) used by zero-detection and the generic nonvanishing-minor layer.
In the broader Recognition framework this sits in the verification domain rather than the forcing chain (T0–T8): it underwrites finite-data reconstructibility of window observables, not the derivation of $\varphi$, the eight-tick octave, or $D=3$. Claim strength stays explicit; the nondegenerate layer is still gated by the separate NonvanishingMinorHypothesis bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.