JcostN_nonneg
plain-language theorem explainer
Non-negativity of the n-dimensional reciprocal cost JcostN holds for arbitrary natural n and real vectors α, x. Researchers extending the scalar Recognition Science cost kernel to multi-component models cite this when verifying positivity in vector settings. The proof is a one-line wrapper that rewrites JcostN via its equivalence to scalar Jcost on the aggregate and applies the scalar non-negativity lemma to the positive aggregate.
Claim. $0 ≤ JcostN(α, x)$ for any natural number $n$ and vectors $α, x ∈ ℝ^n$, where JcostN(α, x) is the n-dimensional cost obtained by applying the scalar J-cost to the weighted geometric-mean aggregate of the components.
background
The module Cost.Ndim.Core lifts the scalar reciprocal cost to n dimensions via a weighted log aggregate. Vec n is the type Fin n → ℝ of n-component real vectors. The aggregate function is defined as exp(∑ α_i log x_i) and is always positive. JcostN α x is defined via JlogN α (logVec x) but equals the scalar Jcost applied to this aggregate.
proof idea
The proof rewrites JcostN α x using the equivalence JcostN_eq_Jcost_aggregate, reducing it to Jcost(aggregate α x). It then applies the lemma Jcost_nonneg to the strictly positive aggregate supplied by aggregate_pos α x.
why it matters
This result is invoked inside the submultiplicativity lemma JcostN_submult in the DAlembert module to bound costs of products. It supplies the positivity step for the n-dimensional cost extension, consistent with scalar non-negativity from J-uniqueness (T5) and the Recognition Composition Law. It closes the non-negativity requirement in the cost chain without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.