pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Cost.Ndim.Symmetry

show as:
view Lean formalization →

The Cost.Ndim.Symmetry module establishes that coefficients in N-dimensional cost calibration remain unchanged under index permutations and proves their equivalence to uniform coefficients. Researchers calibrating symmetric weights in the Recognition Science cost framework cite this result to enforce index-independent uniformity. The module structure consists of a definition of the invariance property together with two direct implications drawn from the upstream calibration relations.

claimA coefficient vector $(c_i)$ satisfies permutation invariance when $c_i = c_j$ for all indices $i,j$, equivalently when $c_i$ is constant across all permutations of the indices. This property holds if and only if the vector is uniform.

background

The module belongs to the Cost domain and imports the Calibration module, whose relations supply the uniform-weight base case. It introduces the permutation-invariance property for coefficients in the N-dimensional setting, where uniformity of weights is the reference configuration. The local theoretical setting treats coefficients as elements of a calibrated cost function whose symmetry must be independent of arbitrary index ordering.

proof idea

The module defines the invariance property as equality of all coefficients under arbitrary index reordering. It then proves that uniform coefficients satisfy the property by direct substitution and conversely that any invariant coefficient vector must be uniform, both steps relying on the calibration relations imported from the upstream module.

why it matters in Recognition Science

This module supplies the symmetry foundation required for consistent cost calculations in the N-dimensional framework. It ensures that uniform weights are the unique choice compatible with index permutation, feeding into higher-level cost structures that rely on calibrated uniformity. The result closes a basic symmetry requirement in the cost calibration chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)