trivialKernel_iff_fullColumnRank
plain-language theorem explainer
For a real matrix, the measurement map has trivial kernel exactly when it is injective (full column rank in the finite-data sense). CPT window reconstruction arguments cite this to move freely between kernel and injectivity language. The proof is a two-direction chain through the intermediate Identifiable predicate, composing the two existing iff lemmas.
Claim. For any real matrix $A \in \mathbb{R}^{m \times n}$, $\ker(\text{measurement map of } A) = \{0\}$ if and only if the measurement map of $A$ is injective.
background
The CPT Window Identifiability module packages the linear-algebra core of finite-window reconstruction: a real matrix $A$ induces a measurement linear map, and identifiability means that map is injective, so window data uniquely determine the input.
Two equivalent formulations are named explicitly. Trivial kernel means the kernel of the measurement map is the zero subspace. Full column rank, in this finite-data sense, is defined as injectivity of that same map (not a rank-number comparison). A third predicate, Identifiable, sits in the middle of the equivalence triangle.
The module also records zero-detection under identifiability and isolates generic nondegeneracy as an explicit NonvanishingMinorHypothesis bundle, so claim strength stays visible.
proof idea
Bidirectional constructor proof. Left-to-right: assume trivial kernel, apply the reverse of identifiable-iff-trivial-kernel to reach Identifiable, then the forward direction of identifiable-iff-full-column-rank. Right-to-left: reverse the same two arrows. No new linear algebra is proved here; both legs are pure composition of the two sibling equivalences (one of which is definitional rfl).
why it matters
Closes the remaining edge of the three-way equivalence among Identifiable, trivial kernel, and full column rank in the CPT window stack. Downstream zero-detection and generic-identifiability arguments can therefore state hypotheses in whichever of the three languages is locally natural without re-proving transport.
In the broader Recognition verification layer this is bookkeeping, not a forcing-chain step: it does not touch T5–T8, the RCL, or the mass ladder. It does keep the matrix-level reconstruction interface coherent so later CPT window claims can cite a single, proved bridge rather than ad hoc rewrites. No used_by edges are recorded yet; the immediate consumers are the sibling zero-detection and nonvanishing-minor results in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.