Pith. sign in
module module high

IndisputableMonolith.Cost.Ndim.Symmetry

show as:
view Lean formalization →

The Cost.Ndim.Symmetry module establishes that coefficients remain unchanged under index permutations in N-dimensional cost models. Researchers formalizing uniform-weight calibrations in Recognition Science would cite it for symmetry properties. The module consists of definitions and basic lemmas that import and extend the Calibration relations without complex internal proofs.

claimCoefficients \(c = (c_1, \dots, c_n)\) satisfy \(c_{\sigma(i)} = c_i\) for every permutation \(\sigma\) of the indices.

background

This module sits in the Cost domain of Recognition Science and imports the Calibration module, whose documentation states it supplies calibration relations for uniform weights. The central object is the permutation-invariance property of coefficients, captured by the sibling declaration CoeffPermutationInvariant together with the two implication lemmas that relate it to uniformity.

proof idea

This is a definition module, no proofs. It introduces the invariance property and supplies the two direction lemmas that equate permutation invariance with the uniform-coefficient condition imported from Calibration.

why it matters in Recognition Science

The module supplies the symmetry layer required for consistent N-dimensional cost constructions. It feeds the broader cost-calibration apparatus that rests on the uniform-weight relations of the imported Calibration module and aligns with the framework's use of uniform coefficients in the phi-ladder and forcing-chain setting.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)