Cost Ndim Dalembert

The multidimensional d'Alembert identity

The multidimensional d'Alembert identity is a theorem in Recognition Science about the recognition cost function JcostN, which measures the forced cost of recognizing one vector relative to another. The theorem states that for any positive vectors x and y of the same length n, the cost of their componentwise product plus the cost of their componentwise quotient equals twice the cost of x plus twice the cost of y plus twice the product of those two costs. In symbols: JcostN (x*y) + JcostN (x/y) = 2 JcostN x + 2 JcostN y + 2 (JcostN x)(JcostN y). This is established in Lean 4 in the module IndisputableMonolith/Cost/Ndim/DAlembert.lean, with no additional axioms beyond the kernel's standard three.

The identity is a structural constraint on how the cost function behaves under the two basic ways of combining positive vectors. It is named after the classical d'Alembert equation because its form resembles the functional equation that characterizes quadratic functions. In the multidimensional setting, the theorem holds for every dimension n and every choice of the scaling parameter α, provided all components are positive. The proof uses the one-dimensional cost identity together with the componentwise definitions of the vector operations.

A direct consequence is a bound on the cost of a product: the cost of the componentwise product of x and y is at most twice the cost of x plus twice the cost of y plus twice the product of the two costs. This follows because the quotient term in the identity is nonnegative, so dropping it gives an inequality. The bound is established as the lemma JcostN_submult in the same module. It gives a quantitative control on how recognition cost can grow when two vectors are combined multiplicatively, which is useful in later arguments about composition and scaling.

The identity does not by itself force a numerical value for JcostN; it is a relation that any cost function satisfying the framework's axioms must obey in all dimensions. It complements the scalar uniqueness theorem by extending the algebraic structure to vectors. The theorem is a established fact about the cost function, not an empirical claim or a modeling choice.

THEOREM JcostN_dAlembert · IndisputableMonolith/Cost/Ndim/DAlembert.lean

THEOREM JcostN_submult · IndisputableMonolith/Cost/Ndim/DAlembert.lean

What this page does not claim

This page does not claim that the identity assigns a numerical value to the cost function. This page does not claim that the identity is an empirical measurement. This page does not claim that the identity holds for vectors with zero or negative 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/DAlembert.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: