JcostN_unit
plain-language theorem explainer
The n-dimensional reciprocal cost vanishes when the input vector is the constant function equal to one, for arbitrary weights. This is the direct lift of the scalar normalization Jcost(1) = 0 to the vector setting. Researchers extending the Recognition Science cost kernel to multiple components would cite this to anchor their definitions at the identity. The proof is a single simplification that unfolds the definitions and applies the scalar unit lemma.
Claim. For any natural number $n$ and any weight vector $α : Fin n → ℝ$, the $n$-dimensional cost satisfies $JcostN(α, 1) = 0$, where $1$ denotes the constant vector with every entry equal to one.
background
The module defines n-dimensional vectors as maps from Fin n to the reals. The cost JcostN(α, x) is obtained by applying the componentwise logarithm to x, taking the weighted dot product with α, exponentiating the result, and feeding that scalar into the original Jcost function. This lifts the scalar kernel through a logarithmic aggregate, as stated in the module header.
proof idea
The proof is a one-line wrapper that applies the simplifier to the definitions of JcostN, JlogN, dot, logVec, and the scalar lemma Jcost_unit0. Unfolding reduces the constant-one vector to the zero vector under logVec, the dot product to zero, the exponential to one, and the outer Jcost to zero.
why it matters
This result supplies the normalization property for the n-dimensional cost at the identity vector, mirroring the scalar fact that Jcost(1) = 0. It anchors the multi-component extension in the Cost.Ndim.Core module and ensures consistency with the underlying Recognition Science cost kernel. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.