JcostN_eq_zero_iff
plain-language theorem explainer
The n-dimensional reciprocal cost vanishes if and only if the dot product of the weighting vector with the coordinate logarithms is zero. Extensions of the scalar cost model to multiple dimensions rely on this equivalence to translate zero-cost conditions into linear relations in logarithmic space. The proof reduces the vector statement to the scalar zero lemma by unfolding the aggregate definition and substituting the dot product term.
Claim. For vectors $α, x ∈ ℝ^n$, the n-dimensional cost $J_N(α, x)$ equals zero if and only if the weighted sum $∑_{i=1}^n α_i log x_i = 0$, where $J_N$ is defined via the logarithmic J-cost applied to the dot product of $α$ and $log x$.
background
Vectors in n dimensions are maps from the finite set of indices to the reals. The n-dimensional cost is obtained by first taking the coordinate-wise logarithm of the positive vector x and then applying the scalar logarithmic cost Jlog to the weighted dot product with the parameter vector alpha. The scalar Jlog satisfies Jlog(t) = 0 exactly when t = 0, as established by the upstream lemmas in the Cost module and its FlogEL and Jlog variants. This module focuses on lifting the scalar kernel through the weighted log aggregate to handle multi-component cases. Upstream results include the definition Jlog(t) := Jcost(exp t) and the equivalence Jlog t = 0 ↔ t = 0, which hold across several implementations of the base cost.
proof idea
The argument is a one-line wrapper: it unfolds JcostN and JlogN, then invokes the scalar Jlog_eq_zero_iff on the specific term given by the dot product of alpha and the log-vector of x, using a simpa tactic to simplify the resulting equivalence.
why it matters
This equivalence is invoked directly by the neutrality theorem that restates zero-cost as the vanishing of the weighted log sum. It supports the reduction of cost conditions in the n-dimensional setting, aligning with the framework's use of the J-uniqueness property and the composition law for extending to higher dimensions. The result completes the core characterization needed for neutrality statements without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.