Cost Ndim Core Jcost N Reciprocal

The reciprocal cost

The declaration JcostN_reciprocal is a machine-checked statement about a cost function built from a weighted log aggregate. The cost function, written JcostN, takes a vector of positive numbers and a vector of weights, and returns a nonnegative real number. The theorem says that if you replace every component of the input vector by its reciprocal, the cost is unchanged: JcostN α (1/x) = JcostN α x. In plain terms, the cost of a configuration and the cost of its componentwise inverse are equal.

The proof is short and relies on the defining formula. The cost is defined as Jcost(exp(Σ αᵢ log xᵢ)), which simplifies to cosh(Σ αᵢ log xᵢ) − 1. Since the hyperbolic cosine is an even function, replacing log xᵢ by −log xᵢ leaves the argument unchanged in sign and the cosine unchanged. The theorem also implies that the cost is zero exactly when the weighted sum of logarithms is zero, which is a separate statement in the same module.

This is a structural property, not an empirical one. It does not say that the cost is the only one with this symmetry, nor that the weights α are determined by anything. It does not claim that the cost is invariant under other transformations, such as scaling all components by a constant. The theorem is a lemma in a larger framework that derives physical constants from a forced cost function, but this declaration alone establishes only the reciprocal symmetry for this particular construction.

In the context of the framework, this symmetry is a building block. The framework models a ledger of recognition events where the cost of recognition is forced by five conditions, and this vector version extends the scalar cost to multiple components. The reciprocal property is one of the conditions that the scalar cost satisfies, and this theorem shows the vector extension inherits it. The payoff is that any later result using this cost can rely on the symmetry without rechecking it.

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

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

What this page does not claim

The theorem does not establish uniqueness of the cost function. The theorem does not determine the weights α from any principle. The theorem does not claim invariance under scaling all components by a constant.

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: