Cost Ndim Core

N-dimensional cost core

Cost ndim core is the module that extends the scalar reciprocal cost to vectors of many components. The scalar kernel cost, the forced mismatch formula J(x) = (x + 1/x)/2 - 1, applies to a single positive number. The n-dimensional version applies it to a whole vector of positive numbers by first compressing the vector into one number through a weighted log aggregate, then feeding that single number into the scalar cost.

The aggregate is the exponential of a weighted sum of componentwise logarithms, R(x) = exp(∑ αᵢ log xᵢ). The weights αᵢ are part of the definition, not derived. The n-dimensional cost is then JcostN(α, x) = J(R(x)). This construction is a definitional choice, tagged MODEL, not a theorem. What the module establishes are the properties that follow from this choice.

The established properties mirror the scalar case. The cost is zero exactly when the weighted log aggregate is zero, and it is always non-negative. It is reciprocal: inverting every component leaves the cost unchanged. The aggregate of a componentwise product splits into a sum of log aggregates, and the same holds for quotients and inverses. These facts are theorems in the machine-checked library, carrying the THEOREM tag.

The key structural result is that the n-dimensional cost equals cosh of the weighted log sum minus one, JcostN = cosh(∑ αᵢ log xᵢ) - 1. This is the same cosh form the scalar cost takes. The multi-component cost therefore inherits the scalar kernel's shape after the log aggregate does its work. This is what the module establishes in plain language: the n-dimensional cost is not a new kind of cost, it is the one forced cost applied to a compressed summary of the vector.

THEOREM JcostN_eq_zero_iff · IndisputableMonolith/Cost/Ndim/Core.lean

THEOREM JcostN_nonneg · IndisputableMonolith/Cost/Ndim/Core.lean

THEOREM JcostN_reciprocal · IndisputableMonolith/Cost/Ndim/Core.lean

THEOREM JcostN_eq_cosh_logsum · IndisputableMonolith/Cost/Ndim/Core.lean

What this page does not claim

The weights αᵢ are not derived; they are part of the definition. This module does not prove that the n-dimensional cost is the unique cost satisfying any set of conditions. No claim is made here about how this cost connects to spatial dimensions or particle structure.

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: