aggregate_pos
plain-language theorem explainer
The aggregate function, defined as the exponential of the weighted dot product of α with the componentwise log of x, is strictly positive for every finite n and all real vectors α, x. Researchers lifting scalar J-cost to n dimensions cite it to guarantee the lifted kernel stays positive and well-defined. The proof is a one-line term-mode reduction that unfolds the aggregate definition and invokes the universal positivity of the real exponential.
Claim. For every natural number $n$ and every pair of vectors $α, x : ℝ^n$, the aggregate $R(α, x) := exp(α · log x)$ satisfies $0 < R(α, x)$, where · denotes the weighted dot product.
background
This module lifts the scalar reciprocal cost to n dimensions by replacing the scalar argument with a weighted logarithmic aggregate. The type Vec n is the function space Fin n → ℝ. The aggregate is defined as Real.exp (dot α (logVec x)).
proof idea
The proof is a one-line term-mode wrapper. It unfolds the aggregate definition to expose the exponential and applies the library lemma that the exponential of any real number is positive.
why it matters
It is invoked by JcostN_nonneg to obtain non-negativity of the n-dimensional cost and by forced_of_scalar_uniqueness to lift scalar uniqueness to vectors. It also appears in the Hessian determinant formulas of det_xHessianMatrix2_formula and det_xHessianMatrix2_ne_zero_of_generic. In the Recognition framework it secures positivity of the multi-component cost kernel used from T5 (J-uniqueness) onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.