Vec
plain-language theorem explainer
n-component real vectors serve as the coordinate representation for multi-dimensional reciprocal costs. Researchers extending scalar J-cost to vector aggregates in Recognition Science reference this abbreviation when building quadratic approximations. The definition is a straightforward type alias from finite indices to reals with no additional structure imposed.
Claim. Let $V(n)$ denote the space of real-valued functions on the finite index set of size $n$, equivalently the set of $n$-tuples of real numbers.
background
The module introduces core definitions for N-dimensional reciprocal cost by lifting the scalar kernel through a weighted log aggregate. Vectors enable componentwise logarithms and weighted sums that generalize the one-dimensional J-cost. The weighted dot product is defined as the sum over components of alpha_i times t_i, which feeds directly into the exponential aggregate R(x) = exp(sum alpha_i log x_i). This setup operates in the context of extending the Recognition Science cost framework to higher dimensions while preserving the reciprocal properties.
proof idea
The declaration is a direct abbreviation equating the vector type to the function space from a finite index set of size n to the reals, serving as the foundational type for all subsequent vector operations in the module.
why it matters
This type definition supports the family of quadratic cost decompositions in the Bridge submodule, such as additive_decomposition which equates additive and multiplicative quadratics plus compensation. It enables the Cauchy-Schwarz style bounds and nonnegativity results used in calibration of the N-dimensional model. Within the broader framework it facilitates the application of the Recognition Composition Law to vector inputs without altering the underlying phi-based constants or dimension D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.