Vec
plain-language theorem explainer
Real vectors indexed by an arbitrary type ι are coordinate maps ι → ℝ. CPT window identifiability and the n-dimensional cost/block-reduction stack both use this as the ambient linear space for measurement maps, kernels, and projectors. The declaration is a one-line type synonym, not a theorem.
Claim. For any index type $\iota$, write $\mathrm{Vec}(\iota) := \iota \to \mathbb{R}$ for the space of real-valued coordinate functions on $\iota$.
background
The CPT Window Identifiability module sets up the matrix-level core for reconstructing states from finite window measurements: injectivity of the measurement map, equivalence with trivial kernel, a full-column-rank predicate (defined as injectivity), and zero-detection under identifiability. A named nonvanishing-minor hypothesis keeps the generic layer explicit.
This abbreviation is the ambient vector type for that story. It generalizes the fixed-dimension version in Cost.Ndim.Core, where vectors are Fin n → ℝ ("n-component real vectors as coordinate functions"). Here the index type is free, so the same notation covers both finite windows and the Fin-based cost geometry used downstream.
Linear measurement maps, kernels, and rank conditions are then predicates on maps between such coordinate spaces, not on abstract modules.
proof idea
No proof. The body is a pure type synonym: Vec ι unfolds definitionally to the function type ι → ℝ. Downstream code treats vectors as pointwise real functions and uses ordinary function extensionality and pointwise algebra.
why it matters
Almost every linear-algebraic object in the CPT window stack is typed over this space: measurement maps, identifiability, trivial kernel, and full column rank. The same synonym is reused heavily in Cost.Ndim.BlockReduction for the undeformed metric inverse Dinv, standard basis covectors e, two-sparse supports, and the block-reduction identity that equates the (i0,i0) entry of the n-dimensional projector P_λ with the 2D closed form P00Gen.
That identity is the algebraic content of "the n-dimensional projector reduces to the 2D one on the 2-sparse slice" and feeds the general-n non-parallelism statement (Theorem 1a style) used in recognition-cost geometry. The abbreviation is scaffolding for notation, not a physics claim; it keeps window CPT and Ndim cost in one coordinate language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.