JcostN
plain-language theorem explainer
The definition JcostN lifts the scalar J-cost kernel to n dimensions by evaluating it at the exponential of the weighted sum of componentwise logs. Researchers extending Recognition Science cost properties to vector inputs cite this when establishing aggregation identities or non-negativity for multi-component systems. It is realized as a direct one-line composition of the log-coordinate cost JlogN with the componentwise logarithm map logVec.
Claim. The n-dimensional positive-coordinate cost is defined by $JcostN(α, x) := Jcost(exp(α · log x))$, where log x is the componentwise natural logarithm, α · t denotes the weighted dot product over the n components, and Jcost is the underlying scalar kernel.
background
The module defines the multi-component reciprocal cost by lifting the scalar kernel through a weighted log aggregate. Vec n is the type of n-component real vectors, realized as functions Fin n → ℝ. logVec applies the natural logarithm to each component, while JlogN evaluates the scalar Jcost at the exponential of the dot product of the weight vector α with a log-coordinate vector t.
proof idea
The definition is a one-line wrapper that applies JlogN to logVec x. It delegates the computation to the scalar Jcost applied to the exponential of the weighted log sum, with no additional tactics or reductions required.
why it matters
This definition is the core lifting of the scalar cost to n dimensions and is invoked by thirteen downstream results, including JcostN_eq_Jcost_aggregate, JcostN_eq_cosh_logsum, JcostN_nonneg, JcostN_reciprocal, and JcostN_eq_zero_iff. It supplies the original positive-coordinate n-dimensional cost in the Ndim.Core module and supports the extension of Recognition Science cost identities to vector settings within the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.