WINDOW_identifiable_iff_fullColumnRank
plain-language theorem explainer
For a real m-by-n measurement matrix, window identifiability is equivalent to full column rank: both mean the induced linear map is injective. Anyone citing paper Theorem 4.5 on CPT window reconstruction can point here. The export is a one-line re-export of the core iff, which holds by definitional equality of the two predicates.
Claim. For any real matrix $A \in \mathbb{R}^{m \times n}$, the measurement map induced by $A$ is injective if and only if $A$ has full column rank in the finite-data sense (injectivity of that same linear map). Equivalently, window identifiability of $A$ holds exactly when $A$ has full column rank.
background
This sits on the CPT export surface: citation-friendly aliases for the fully proved CPT formalization (no sorry, no new axioms). The WINDOW_* family maps to paper Theorems 4.5 and 6.5 on window identifiability.
In the window model, a real matrix $A$ induces a linear measurement map on finite-dimensional data. Identifiability means that map is injective: distinct latent configurations produce distinct observations. Full column rank is defined the same way in this layer: injectivity of the matrix-induced linear map, not a separate rank-number predicate.
Upstream, both predicates are literally Function.Injective (measurementLinear A). The core lemma therefore collapses by reflexivity. The two A constants pulled from GapDerivation and Masses.Anchor are ambient RS edge-count notation and do not enter the logical content of this equivalence.
proof idea
One-line term wrapper: apply WindowIdentifiability.identifiable_iff_fullColumnRank to $A$. That core theorem is itself proved by rfl, because Identifiable A and FullColumnRank A are definitionally the same proposition (injectivity of measurementLinear A). No algebraic rank computation is performed here.
why it matters
Paper Theorem 4.5 needs a stable, citable name linking the reconstruction language (identifiability) to the linear-algebra language (full column rank). This export supplies that bridge for the WINDOW family without adding proof burden.
Sibling exports (WINDOW_identifiable_iff_trivialKernel, WINDOW_zero_detection_of_identifiable) and the CPT pipeline / optimality / forced-factorization aliases sit beside it on the same surface. Downstream use count is currently empty on this graph edge set, so the declaration is primarily a citation and composition hook rather than an intermediate lemma in a longer chain.
Within Recognition Science verification, it certifies that the finite-window measurement model has a clean injectivity criterion before noise ($\varepsilon$) and optimality layers are stacked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.