pith. sign in
module module high

IndisputableMonolith.Cost.Ndim.Neutrality

show as:
view Lean formalization →

Cost.Ndim.Neutrality supplies the neutrality equivalences for the N-dimensional reciprocal cost. The central claim states that aggregate equals one exactly when the weighted log sum is zero. Researchers analyzing multi-component systems in Recognition Science cite these equivalences to confirm cost balance. The results follow by direct expansion of the weighted aggregate definition imported from Core.

claim$aggregate(w, x) = 1$ if and only if the weighted sum of logarithms vanishes: $sum_i w_i log x_i = 0$, for weights $w$ and positive components $x$.

background

The module extends the scalar reciprocal cost to N dimensions by lifting the scalar kernel through a weighted log aggregate, as defined in the Core module. This construction preserves the composition properties of the underlying J-cost while allowing vector inputs.

proof idea

The module contains direct equivalences derived from the aggregate definition. Each result follows by algebraic expansion of the weighted log sum and application of logarithm properties, with no additional lemmas required beyond the Core import.

why it matters in Recognition Science

The neutrality results anchor the N-dimensional cost construction in the Recognition framework and ensure consistency with the scalar case. They support later results on cost minimization and dimensional independence, though no immediate downstream declarations are recorded.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)