aggregate
plain-language theorem explainer
The aggregate definition supplies the n-dimensional exponential cost R(α, x) = exp(∑ α_i log x_i) for vectors in ℝ^n. Researchers extending scalar J-cost to weighted multi-component models cite it when constructing log-aggregates for recognition events. The definition is a direct composition of the weighted dot product on the componentwise logarithm followed by real exponentiation.
Claim. For vectors α, x ∈ ℝ^n the aggregate is defined by R(α, x) := exp(∑_{i=1}^n α_i log x_i).
background
The module defines n-dimensional reciprocal cost by lifting the scalar kernel through a weighted log aggregate. Vec n is the type of n-component real vectors, represented as functions Fin n → ℝ. The dot operation computes the weighted sum ∑ α_i t_i while logVec applies the natural logarithm componentwise.
proof idea
The definition is a direct one-line composition that applies the weighted dot product to the componentwise logarithm of x and then takes the real exponential.
why it matters
This definition forms the foundation for the n-dimensional J-cost and feeds directly into JcostN_eq_Jcost_aggregate and aggregate_pos. It realizes the multi-component extension of the recognition cost while preserving the exponential aggregate structure from the scalar case in MultiplicativeRecognizerL4.cost and ObserverForcing.cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.