NonvanishingMinorHypothesis
plain-language theorem explainer
Named hypothesis bundle for the paper's generic (nondegenerate) CPT-window regime: a real measurement matrix is assumed to have full column rank, meaning its induced linear map is injective. Anyone citing generic window identifiability from a verified nonvanishing maximal minor uses this bridge. It is a one-field Prop structure, not a proved statement.
Claim. For a real $m \times n$ matrix $A$, the nonvanishing-minor hypothesis holds when $A$ has full column rank in the finite-data sense: the linear map $x \mapsto A x$ is injective.
background
The CPT window-identifiability module treats reconstruction from finite window measurements as a linear-algebra problem. Identifiability means injective recovery of the unknown vector from the measurement matrix; that property is equivalent to a trivial kernel and to a full-column-rank predicate defined here as injectivity of the matrix-induced map.
Full column rank is not the classical determinant criterion in this file: it is defined as injectivity of measurementLinear A. The module keeps the paper's "generic/nondegenerate" layer explicit by packaging that injectivity assumption under a named hypothesis rather than silently assuming minors are nonzero.
Upstream anchors such as the active-edge count $A = 1$ sit in the broader RS mass and gap calculus; they are not used in the body of this structure, which is purely matrix-level.
proof idea
No proof body: this is a Prop-valued structure with a single field. That field is exactly the full-column-rank predicate (injectivity of the measurement map). Instantiating the hypothesis means supplying a proof of injectivity; there is no algebraic reduction or tactic script at this declaration.
why it matters
Keeps claim strength honest in the CPT verification stack. Downstream, generic_identifiability_assuming_nonvanishing_minor is a one-line unwrap: under this hypothesis the matrix is identifiable. The doc-comment states the intent: assume the paper's maximal-minor nonvanishing condition has already been checked elsewhere, and expose only the identifiability consequence at this layer.
In the Recognition framework this sits in the verification domain for CPT window arguments (injective reconstruction, zero-detection under identifiability). It does not itself touch the forcing chain T0–T8, RCL, or the mass ladder; it is infrastructure so those physics claims can cite a clean, named nondegeneracy hypothesis rather than an opaque rank assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.