JlogN_eq_cosh_sub_one
plain-language theorem explainer
The n-dimensional logarithmic cost equals the hyperbolic cosine of the weighted dot product minus one. Researchers extending the Recognition Science scalar cost kernel to vector aggregates would cite this reduction when collapsing multi-component logs to the cosh identity. The proof is a one-line wrapper that unfolds JlogN and applies the scalar lemma Jcost_exp_cosh directly to the dot product value.
Claim. For vectors $α, t ∈ ℝ^n$, the n-dimensional log-cost defined by $J_{log N}(α, t) := Jcost(exp(α · t))$ satisfies $J_{log N}(α, t) = cosh(α · t) - 1$, where $α · t$ denotes the weighted dot product $∑_i α_i t_i$.
background
Module Cost.Ndim.Core lifts the scalar reciprocal cost to n dimensions via a weighted log aggregate. Vectors are coordinate functions Fin n → ℝ. The weighted dot product is defined as the sum over components α_i t_i and serves as the direct argument to the exponential inside the definition of JlogN, which composes Jcost with exp(dot α t).
proof idea
One-line wrapper. It unfolds the definition of JlogN to expose Jcost(exp(dot α t)), then invokes the upstream scalar lemma Jcost_exp_cosh on the real value dot α t, with simpa performing the substitution and simplification.
why it matters
This identity supplies the hyperbolic form for the n-dimensional cost, extending the scalar J-uniqueness (T5) that writes J(x) as cosh(log x) - 1. It closes the basic reduction step in the Cost domain before any further aggregation or ladder constructions. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.