Vec
Vec n is the type of n-component real vectors represented as maps from the finite index set Fin n to the reals. Researchers extending the scalar reciprocal cost kernel to multiple dimensions cite this as the basic coordinate space for weighted aggregates. The declaration is a direct type abbreviation with no further structure or proof obligations.
claimFor each natural number $n$, let $V_n$ denote the set of all functions from the finite set of indices with $n$ elements to the real numbers, serving as the coordinate representation of $n$-dimensional vectors.
background
The module Cost.Ndim.Core introduces the multi-component reciprocal cost by lifting the scalar kernel through a weighted log aggregate. Supporting definitions include the weighted dot product, which sums componentwise products of two vectors, and the exponential aggregate, which recovers a scalar from weights and log-coordinates via the dot product. These rest on the one-dimensional J-cost and Recognition Composition Law from the parent Cost module.
proof idea
The declaration is a direct abbreviation of the function type Fin n to the reals, supplying the vector space of coordinates without additional axioms or lemmas.
why it matters in Recognition Science
This vector type supplies the domain for all N-dimensional cost constructions and feeds directly into the Bridge module theorems, including additive_decomposition, compensatory_nonneg_of_sqNorm_le_one, and multiplicative_le_additive_of_sqNorm_le_one. It extends the scalar J-uniqueness (T5) and phi-ladder structure to higher dimensions while preserving the eight-tick octave and D=3 spatial setting of the Recognition framework. No open scaffolding remains at this level.
scope and limits
- Does not equip the vectors with an inner product or norm beyond coordinate functions.
- Does not define vector addition, scalar multiplication, or componentwise operations.
- Does not enforce positivity of components required for the logarithmic aggregate.
- Does not reference the phi-ladder, mass formulas, or Berry threshold directly.
formal statement (Lean)
18abbrev Vec (n : ℕ) := Fin n → ℝ
proof body
Definition body.
19
20/-- Weighted dot product used by the logarithmic aggregate. -/
used by (40)
-
additive_decomposition -
additiveQuadratic -
compensatory_nonneg_of_sqNorm_le_one -
compensatoryQuadratic -
dot_sq_le_sqNorm_mul -
multiplicative_le_additive_of_sqNorm_le_one -
multiplicativeQuadratic -
sqNorm -
sqNorm_uniform -
uniform_sqNorm_one -
uniform_weight_of_sum_one -
UniformWeights -
weightSum -
weightSum_uniform -
not_projectivelyEquivalentToZeroAt_tPulledConnection -
projectivelyEquivalent_one_dim -
ProjectivelyEquivalentToZeroAt -
tPulledConnection -
tPulledConnection_diag -
tPulledConnection_offDiag -
xFlatConnection -
xFlatConnection_apply -
aggregate -
aggregate_pos -
dot -
dot_log_hadamardDiv -
dot_log_hadamardInv -
dot_log_hadamardMul -
hadamardDiv -
hadamardInv