JcostN_eq_cosh_logsum
plain-language theorem explainer
The n-dimensional cost equals cosh of the weighted dot product between the weight vector and the componentwise logarithm of the input vector, minus one. Workers extending the scalar J-cost kernel to vector inputs cite this reduction to connect multi-component aggregates to the hyperbolic identity. The proof is a direct one-line wrapper that substitutes the aggregate into the scalar exponential form of J.
Claim. For any natural number $n$ and vectors $α, x ∈ ℝ^n$, the n-dimensional cost satisfies $J_N(α, x) = cosh(α · log x) - 1$, where $J_N$ is obtained by composing the scalar cost with the weighted logarithmic aggregate.
background
The module defines n-dimensional reciprocal cost by lifting the scalar kernel through a weighted log aggregate. Vectors are maps from Fin n to reals. The weighted dot product aggregates components as sum α_i t_i. JlogN applies the scalar cost to the exponential of this dot product, while JcostN composes further with componentwise logarithm to recover the original positive-coordinate form.
proof idea
The proof is a one-line wrapper that applies the scalar lemma equating J(exp(t)) to cosh(t) minus one, after substituting the dot product of α with logVec(x) and unfolding the definitions of the n-dimensional cost and its log-coordinate version.
why it matters
This identity feeds the reciprocity theorem under componentwise inversion, which rewrites both sides via the cosh form and uses the negation property of cosh. It embeds the multi-dimensional cost into the hyperbolic representation that underlies the J-uniqueness step of the forcing chain. The module thereby prepares n-dimensional extensions of the cost axioms without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.