Cost Ndim Symmetry

Cost ndim symmetry

Cost ndim symmetry is the property that the coefficient weights of a cost function do not change when their indices are permuted. In plain language, the weights treat every slot in the index list the same way; swapping any two indices leaves the weight assigned to each position unchanged. The property is stated for a vector of coefficients of length n, and it holds when every permutation of the index set preserves the coefficient at each index.

The module establishes an exact equivalence between this symmetry and uniformity. A set of weights is uniform when all entries are equal to a single value. The first theorem shows that uniform weights are always permutation invariant. The second theorem shows the converse: in any positive dimension n, if the weights are permutation invariant, then they must be uniform. The converse is the substantive direction, since it shows that the symmetry condition alone, with no further assumption about the values, forces the weights to be identical.

This equivalence matters because it turns a structural requirement into a concrete constraint. If a cost function in n dimensions is required to respect permutation symmetry, then its coefficient weights are not free to vary; they collapse to one number. The result is established for every positive natural number n, so the forcing is not special to a particular dimension. It is a general statement about what permutation symmetry means for coefficient weights.

THEOREM coeff_perm_invariant_of_uniform · IndisputableMonolith/Cost/Ndim/Symmetry.lean

THEOREM uniform_of_coeff_perm_invariant · IndisputableMonolith/Cost/Ndim/Symmetry.lean

What this page does not claim

This answer does not claim that cost ndim symmetry alone determines the full cost function. This answer does not claim that the equivalence extends to zero dimensions. This answer does not claim that permutation symmetry applies to anything beyond coefficient weights.

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/Symmetry.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: