Cost Ndim Core Jcost N Eq Cosh Logsum

The cost in many dimensions

The declaration JcostN_eq_cosh_logsum is a proved theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that the multi-component cost JcostN, which measures the price of a recognition event involving several components at once, equals Real.cosh (dot α (logVec x)) - 1. In plainer terms: take each component of the vector x, replace it by its natural logarithm, form the weighted sum with the weights α, apply the hyperbolic cosine function, and subtract one. The result is the cost.

The formula is not plucked from nowhere. It is a direct consequence of the scalar cost theorem Jcost_exp_cosh, which the framework proves from its five plain conditions on cost functions. The scalar result says that for a single positive number, the cost equals cosh(log x) - 1, which simplifies to (x + 1/x)/2 - 1. The multi-component version lifts this through a weighted log aggregate: the aggregate R(x) = exp(∑ αᵢ log xᵢ) compresses the vector into a single positive number, and the cost of the vector is just the scalar cost of that aggregate. The theorem JcostN_eq_cosh_logsum makes the compression explicit by writing the cost directly in terms of the log-coordinate dot product.

This compact form carries real content. From it, the framework derives that the cost is zero exactly when the weighted log sum is zero, that the cost is always non-negative, and that it is unchanged when every component of x is replaced by its reciprocal. The reciprocal symmetry is visible in the formula: negating the log sum leaves the hyperbolic cosine unchanged. These properties are what make the multi-component cost a faithful extension of the scalar one, rather than an arbitrary choice.

What the theorem does not claim is just as important. It does not assert that this cost function is the only possible one in higher dimensions; the uniqueness theorem applies to the scalar case. It does not assign physical meaning to the weights α or to the components of x; those are modeling choices. And it does not say that the formula holds for negative or zero components, since logarithms require positive inputs. The theorem is a structural identity, not a statement about what the world contains.

theorem JcostN_eq_cosh_logsum {n : ℕ} (α x : Vec n) :
    JcostN α x = Real.cosh (dot α (logVec x)) - 1 := by
  simpa [JcostN, JlogN] using (Jcost_exp_cosh (dot α (logVec x)))

/-- Zero-cost characterization in log coordinates. -/
theorem JcostN_eq_zero_iff {n : ℕ} (α x : Vec n) :
    JcostN α x = 0 ↔ dot α (logVec x) = 0 := by
  unfold JcostN JlogN
  simpa [Jlog] using (Jlog_eq_zero_iff (t := dot α (logVec x)))

/-- Non-negativity follows from scalar non-negativity at positive aggregate. -/
theorem JcostN_nonneg {n : ℕ} (α x : Vec n) : 0 ≤ JcostN α x := by
  rw [JcostN_eq_Jcost_aggregate]
  exact Jcost_nonneg (aggregate_pos α x)

/-- Reciprocity under componentwise inversion. -/
theorem JcostN_reciprocal {n : ℕ} (α x : Vec n) :
    JcostN α (hadamardInv x) = JcostN α x := by
  rw [JcostN_eq_cosh_logsum, JcostN_eq_cosh_logsum]
  rw [dot_log_hadamardInv, Real.cosh_neg]

What this page does not claim

The theorem does not prove uniqueness of the multi-component cost function. The theorem does not assign physical meaning to the weights or components. The formula does not apply to vectors with non-positive components.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/Ndim/Core.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: