aggregate_eq_one_iff
plain-language theorem explainer
The equivalence states that for vectors α and x the exponential aggregate equals one precisely when the weighted sum of logarithms vanishes. Analysts working on n-dimensional cost neutrality in Recognition models cite this when reducing zero-cost conditions to a vanishing dot product. The tactic proof unfolds the aggregate definition then applies exponential injectivity forward and direct simplification backward.
Claim. $R(x) = 1$ if and only if the weighted logarithmic sum vanishes, where $R(x) = exp(∑ α_i log x_i)$ for vectors α, x in ℝ^n.
background
The module treats the ledger neutrality surface for n-dimensional cost models. Vec n is the type of n-component real vectors as maps from Fin n to reals. Aggregate is the exponential of the dot product of α with the componentwise logarithm of x. Dot computes the weighted sum ∑ α_i t_i. LogVec applies the real logarithm componentwise. Upstream definitions include the aggregate construction from Core and the cost functions induced by multiplicative recognizers and observer forcing events.
proof idea
The proof unfolds aggregate to expose exp(dot α (logVec x)). It splits the biconditional via constructor. The forward direction simplifies to equality of exponentials at zero then invokes real exponential injectivity. The reverse direction applies direct simplification on the hypothesis.
why it matters
This equivalence supports the zero-cost iff aggregate-one theorem in the same module, which links vanishing J-cost to aggregate equaling one. It supplies a neutrality step inside the cost ledger, connecting to the Recognition framework where costs arise from multiplicative recognizers and observer forcing. The result closes a local reduction without touching open questions on higher-dimensional extensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.