pith. sign in
module module high

IndisputableMonolith.Cost.Ndim.Core

show as:
view Lean formalization →

The Cost.Ndim.Core module defines n-component real vectors and their coordinate operations for extending the scalar J-cost to multiple dimensions in Recognition Science. Multidimensional cost researchers cite it for the vector primitives that enable later identities. The module consists solely of definitions with no proofs or theorems.

claimThe module introduces the space of n-component vectors $V_n = (x_1, ..., x_n) $ with $x_i > 0$, equipped with the inner product $u · v = sum u_i v_i$, componentwise logarithm $log V$, Hadamard product $u ⊙ v$, and the derived n-dimensional functions $JlogN(V)$ and $JcostN(V)$ that generalize the scalar J-cost.

background

This module belongs to the Cost domain and imports the scalar cost primitives from IndisputableMonolith.Cost. It supplies the vector layer required for n-dimensional extensions by defining Vec as n-tuples of positive reals, dot as the standard sum-of-products inner product, logVec as the componentwise logarithm, and the Hadamard family (hadamardMul, hadamardInv, hadamardDiv) for elementwise arithmetic. Aggregate sums the components while JlogN and JcostN lift the one-dimensional J function to vectors, with the relation JlogN_eq_cosh_sub_one linking them to the hyperbolic form.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the vector coordinate foundation required by all downstream Ndim modules: Bridge for additive-multiplicative quadratic relations, Calibration for uniform-weight identities, Connections for affine Christoffel terms in log-coordinates, DAlembert for the multidimensional RCL identity, Hessian for second-derivative formulas, Neutrality for ledger surfaces, Octave, and RicciScalar. It thereby enables the n-dimensional generalization of the Recognition Science cost that supports the forcing chain from T5 onward.

scope and limits

used by (10)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (20)