Cost Ndim Uniqueness

The n-dimensional uniqueness lift

Cost ndim uniqueness is the theorem that extends the forced form of the recognition cost (the unique mismatch formula J(x) = (x + 1/x)/2 - 1) from a single scalar input to a vector of n components. The module establishes a forcing pattern: if a candidate function F on n positive reals factors through a weighted multiplicative aggregate, and if the scalar factor G is uniquely fixed to Jcost on positive reals, then F must equal JcostN, the n-dimensional cost. The result is machine-checked as forced_of_scalar_uniqueness and its existential form forced_of_factorization.

The plain meaning is that no separate n-dimensional cost function needs to be invented. Once the one-dimensional cost is uniquely determined, any n-component candidate that respects the same aggregate structure inherits that uniqueness. The theorem says: if F x = G (aggregate α x) for some scalar profile G, and if G is forced to be Jcost on positive inputs, then F x = JcostN α x for all x. The proof is a two-line calculation: substitute the factorization, apply the scalar uniqueness, and use the definitional identity JcostN = Jcost ∘ aggregate.

The module does not establish that every n-dimensional cost must factor through the aggregate. That factorization is a hypothesis, stated as FactorsThrough. What the module establishes is the lift: given the factorization and the scalar uniqueness, the n-dimensional form is forced. This is the bridge that carries the one-dimensional forcing result into higher dimensions, and it is what makes the rest of the forcing chain (the eight-tick cycle, 2^3, three spatial dimensions) able to use the scalar cost as its engine.

THEOREM forced_of_scalar_uniqueness · IndisputableMonolith/Cost/Ndim/Uniqueness.lean

THEOREM forced_of_scalar_uniqueness · IndisputableMonolith/Cost/Ndim/Uniqueness.lean

THEOREM forced_of_scalar_uniqueness · IndisputableMonolith/Cost/Ndim/Uniqueness.lean

What this page does not claim

This answer does not claim that every n-dimensional cost function factors through the aggregate; that factorization is a hypothesis, not a theorem. This answer does not claim that the scalar uniqueness of Jcost is established in this module; it is assumed as a hypothesis. This answer does not claim that JcostN itself is defined in this module; the module uses it as 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/Uniqueness.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: