Pith. sign in
module module moderate

IndisputableMonolith.Cost.Ndim.Neutrality

show as:
view Lean formalization →

Characterizes neutrality for the N-dimensional reciprocal cost: the weighted log aggregate equals one exactly when the weighted sum of logs vanishes. Supplies the zero-cost equivalences (cost zero iff the log-dot is zero iff the aggregate is one). Anyone working multi-component J-cost or RS mass ladders cites these iff lemmas. Proofs are short algebraic rewrites from the Core aggregate definition.

claimFor the N-dimensional reciprocal cost built from a weighted log aggregate $A$, one has $A=1$ if and only if the weighted sum of logarithms is zero; equivalently the cost vanishes iff that log-dot product is zero iff $A=1$.

background

The parent module Cost.Ndim.Core lifts the scalar reciprocal cost kernel to several components by a weighted log aggregate: components are combined on the log scale with fixed weights, then exponentiated back to a single positive scale factor. That aggregate plays the role of the multi-factor argument to the scalar J-cost.

Neutrality means the multi-component configuration contributes no excess cost: the aggregate sits at the fixed point $1$ of the reciprocal kernel (where $J(1)=0$). In log coordinates this is exactly the statement that the weighted sum of the component logs is zero, i.e. a balanced (zero-mean) log vector under the weight measure.

The three sibling statements package that dictionary: aggregate equals one iff weighted log sum zero; cost zero iff log-dot zero; cost zero iff aggregate one.

proof idea

Definition-level module built on Core. Each lemma is a short algebraic rewrite: unwind the aggregate as $\exp$ of a weighted sum of logs, use $\exp(s)=1\Leftrightarrow s=0$, and compose with the scalar fact that the reciprocal cost vanishes only at argument $1$. No deep induction or analysis; pure equational reasoning from the Core definitions.

why it matters in Recognition Science

In Recognition Science the scalar cost $J$ (forced unique by T5) vanishes only at the neutral point $x=1$. The N-dimensional lift must inherit a clean neutrality criterion so multi-factor configurations (charges, rung gaps, channel weights) can be certified cost-free. These iff lemmas are the bookkeeping layer that lets later cost and mass arguments reduce multi-component balance to a single log-dot condition. Downstream used_by edges are not yet wired in the graph; the natural consumers are any N-dim cost identities and zero-cost classification theorems that sit above Core.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)