Cost Ndim Core Jlog N Eq Cosh Sub One

The log-coordinate cost identity

The declaration JlogN_eq_cosh_sub_one proves that the n-dimensional log-coordinate cost equals cosh(dot product) minus 1. In plain terms, if you take n positive numbers, apply a weighted logarithm to combine them, and then feed that single number into the framework's basic cost function, the result is exactly the hyperbolic cosine of that weighted log sum, minus one. The hyperbolic cosine, written cosh, is the average of an exponential and its reciprocal: cosh(u) = (e^u + e^-u)/2. So the identity says the cost of a multi-component configuration is cosh(u) - 1, where u is the weighted log aggregate.

This identity is a theorem in the machine-checked library of formal theorems, meaning it follows from the definitions by a chain of logical steps that a computer verified. It builds on an earlier scalar result: for a single positive number x, the basic cost J(x) equals cosh(log x) - 1. The n-dimensional version lifts that scalar fact by first compressing the n components into one number through the weighted log aggregate R(x) = exp(sum α_i log x_i), then applying the scalar cost. The proof is a direct substitution using the definition of the log-coordinate cost and the scalar identity.

The identity is not a new physical law and does not add assumptions to the framework. It is a rewriting rule: it shows that the n-dimensional cost, defined as Jcost(exp(dot α t)), can be expressed in the simpler closed form cosh(dot α t) - 1. This matters because it makes the cost's behavior transparent. For small values of the log aggregate u, cosh(u) - 1 is approximately u²/2, so the cost grows quadratically near the identity. For large u, it grows exponentially. The identity also immediately implies two structural facts: the cost is zero exactly when the weighted log sum is zero, and the cost is unchanged if you replace every component by its reciprocal, because cosh is an even function.

In Recognition Science, this identity is one step in a larger program that derives physical constants from the cost function. But the declaration itself does not derive any physical constant, does not mention space or time, and does not claim that the n-dimensional cost is the unique cost satisfying any axioms. It only states an equivalence between two expressions for the same definition. The uniqueness of the scalar cost J is a separate theorem; this declaration assumes that cost and shows what it looks like in log coordinates.

theorem JlogN_eq_cosh_sub_one {n : ℕ} (α t : Vec n) :
    JlogN α t = Real.cosh (dot α t) - 1 := by
  simpa [JlogN] using (Jcost_exp_cosh (dot α t))

theorem JlogN_eq_cosh_sub_one {n : ℕ} (α t : Vec n) :
    JlogN α t = Real.cosh (dot α t) - 1 := by
  simpa [JlogN] using (Jcost_exp_cosh (dot α t))

/-- 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)))

/-- 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 declaration does not derive any physical constant or mention space or time. The declaration does not assert that the n-dimensional cost is unique among all cost functions. The declaration does not introduce new axioms; it only rewrites an existing definition.

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: