identifiable_iff_fullColumnRank
plain-language theorem explainer
For a real measurement matrix, window identifiability is definitionally the same as full column rank: both mean the induced linear measurement map is injective. CPT window reconstruction arguments cite this to switch freely between the two names. The proof is pure definitional equality (rfl).
Claim. For any real matrix $A$ of size $m \times n$, the measurement map induced by $A$ is injective if and only if $A$ has full column rank in the finite-data reconstruction sense (injectivity of that same map).
background
The CPT Window Identifiability module fixes the matrix-level core used in finite-window reconstruction: injective recovery from window measurements, equivalence with a trivial kernel of the measurement map, and a full-column-rank predicate. Identifiability is defined as injectivity of measurementLinear A. Full column rank is defined, in this finite-data sense, as the same injectivity predicate.
The module keeps the generic/nondegenerate layer separate via an explicit NonvanishingMinorHypothesis bundle, so claim strength stays visible. Upstream, the two predicates here are literally the same Prop, which is why switching names is free.
proof idea
One-line definitional proof: both sides unfold to Function.Injective (measurementLinear A), so rfl closes the biconditional. No lemmas are applied.
why it matters
This is the name-bridge inside the CPT window stack. The export WINDOW_identifiable_iff_fullColumnRank re-exports it as paper Theorem 4.5 (identifiability ↔ full column rank). The sibling trivialKernel_iff_fullColumnRank routes through this equivalence together with identifiable_iff_trivialKernel, so the three formulations (identifiable, trivial kernel, full column rank) form a closed triangle.
In the broader Recognition verification layer this supports finite-window injectivity arguments used when reconstructing structure from CPT-style measurements. It does not itself touch the forcing chain (T0–T8) or the mass ladder; it is pure linear-algebra bookkeeping for the window claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.