zero_cost_iff_aggregate_one
plain-language theorem explainer
The equivalence states that the n-dimensional J-cost of vectors α and x vanishes precisely when their exponential aggregate equals one. Workers on neutrality surfaces in the cost ledger would invoke this when verifying zero-cost states. The proof composes two biconditionals, one linking cost to the weighted log-dot product and the other linking the aggregate to the same dot product.
Claim. For vectors $α, x ∈ ℝ^n$, the n-dimensional J-cost satisfies $J_{cost,n}(α,x)=0$ if and only if the exponential aggregate $R(α,x)=exp(α·log x)$ equals one.
background
The module develops the ledger neutrality surface for n-dimensional costs. Vec n denotes the type of n-component real vectors, written as functions from Fin n to ℝ. The aggregate function computes the exponential of the weighted sum of logarithms: R(α,x) = exp(α · logVec x). JcostN(α,x) is defined as the logarithmic cost JlogN α (logVec x). Upstream, aggregate_eq_one_iff records that R(α,x)=1 exactly when the dot product α·logVec x vanishes. Similarly, zero_cost_iff_dot_zero states that JcostN(α,x)=0 if and only if the same dot product is zero.
proof idea
The term proof splits the biconditional with constructor. The forward direction applies zero_cost_iff_dot_zero to obtain the dot product zero, then aggregate_eq_one_iff to reach aggregate equals one. The reverse direction reverses the order of the same two lemmas.
why it matters
This equivalence sits in the ledger neutrality surface and closes the loop between vanishing cost and unit aggregate. It supplies a direct criterion for neutral configurations without explicit computation of the dot product. In the Recognition framework it supports checks that zero cost occurs precisely at the fixed point where the aggregate normalizes to one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.