generic_identifiability_assuming_nonvanishing_minor
plain-language theorem explainer
Under an explicit nonvanishing-maximal-minor hypothesis on a real measurement matrix, the finite-window measurement map is injective. CPT window arguments cite this to turn the paper's generic/nondegenerate regime into formal identifiability. The proof is a one-field projection: the hypothesis bundle already packages full column rank, which is definitionally identifiability in this module.
Claim. Let $A$ be an $m \times n$ real matrix. If $A$ satisfies the nonvanishing maximal-minor hypothesis (the module's bridge for the paper's generic/nondegenerate regime, which asserts full column rank of $A$), then $A$ is window-identifiable: the associated linear measurement map is injective.
background
This module is the matrix-level core of CPT window arguments: injective reconstruction from finite window measurements, equated with trivial kernel of the measurement map and with a full-column-rank predicate defined here as injectivity, plus zero-detection under that injectivity.
Identifiable A means the linear measurement map of $A$ is injective. The generic layer is not proved inside the module; it is packaged as NonvanishingMinorHypothesis A, an explicit Prop-structure whose only field is full column rank of $A$. The module doc states the intent: assume the relevant maximal-minor nonvanishing condition has already been verified, and expose only the identifiability consequence at this layer.
Sibling equivalences (identifiable_iff_trivialKernel, identifiable_iff_fullColumnRank, trivialKernel_iff_fullColumnRank) make the three formulations interchangeable once any one is obtained.
proof idea
One-line term proof. From the hypothesis structure project the field fullColumnRank, which has type FullColumnRank A. In this module full column rank is defined as injectivity of the measurement map, matching Identifiable A definitionally, so no further lemma application is required.
why it matters
Closes the generic-to-identifiable bridge in the CPT verification stack without hiding strength: the paper's nondegenerate regime is named as a hypothesis bundle rather than smuggled into a definition. Downstream consumers (none wired yet in the graph) can assume the minor condition once and obtain injectivity, then use zero-detection and the kernel/rank equivalences for window reconstruction arguments.
It does not itself touch the forcing chain (T0–T8), RCL, or mass ladder; it is infrastructure for CPT window uniqueness claims that sit above those foundations. Keeping the minor condition as a named hypothesis makes any future discharge (or counterexample) of genericity a single, auditable step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.