JcostN_eq_Jcost_aggregate
plain-language theorem explainer
The equality shows that the n-dimensional reciprocal cost JcostN(α, x) coincides with the scalar Jcost applied to the weighted geometric aggregate of the components. Researchers extending the Recognition cost kernel to multiple dimensions cite this reduction to collapse vector calculations to the scalar case. The proof is a direct reflexivity after the definitions of JcostN and aggregate are unfolded.
Claim. For any natural number $n$ and vectors $α, x ∈ ℝ^n$, the n-dimensional cost satisfies $JcostN(α, x) = Jcost(aggregate(α, x))$, where $aggregate(α, x) = exp(α · log x)$ is the exponential of the weighted log-sum.
background
This module defines the multi-component reciprocal cost by lifting the scalar kernel through a weighted log aggregate. Vectors are coordinate functions Vec n := Fin n → ℝ. The aggregate is the exponential of the dot product of α with logVec x, producing a positive scalar that serves as the effective input to the scalar cost. JcostN is defined as JlogN α (logVec x), and the theorem equates this directly to the scalar Jcost on the aggregate value.
proof idea
The proof is a one-line reflexivity that confirms the definitional equality once JcostN and aggregate are unfolded.
why it matters
This reduction is invoked in the non-negativity proof for JcostN and in the main forcing theorem that scalar uniqueness implies the n-dimensional lift. It supplies the bridge from scalar J-cost to the vector case inside the Recognition framework, aligning with the composition law and the phi-ladder construction of masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.