zero_cost_iff_dot_zero
plain-language theorem explainer
The equivalence shows that the n-dimensional J-cost vanishes precisely when the weighted sum of logarithms is zero. Researchers modeling ledger neutrality in Recognition Science cite this to reduce positivity conditions to linear constraints in log space. The proof is a one-line wrapper that invokes the zero-cost characterization already established in log coordinates.
Claim. For vectors $α, x ∈ ℝ^n$, the n-dimensional J-cost $J_{cost,n}(α, x)$ equals zero if and only if the weighted dot product $α · log x = 0$, where the dot product is the sum $∑ α_i log x_i$.
background
The Cost.Ndim.Neutrality module treats the ledger neutrality surface. Vectors are coordinate functions from Fin n to reals. logVec applies the natural logarithm componentwise. dot computes the weighted sum ∑ α_i t_i. JcostN applies the J-log to the log vector, recovering the original positive-coordinate cost. aggregate is the exponential of that same dot product. This theorem rests on JcostN_eq_zero_iff from Core, whose doc-comment states it supplies the zero-cost characterization in log coordinates.
proof idea
The proof is a one-line term wrapper that applies JcostN_eq_zero_iff α x from the Core module.
why it matters
This result supports neutrality theorems by equating cost zero to vanishing of the log-weighted sum. It directly feeds zero_cost_iff_aggregate_one, which rewrites the condition as aggregate α x = 1. The lemma sits inside the ledger neutrality surface and connects to the Recognition framework's cost definitions and multiplicative recognition steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.