CoeffPermutationInvariant
plain-language theorem explainer
Definition CoeffPermutationInvariant states that an n-component real vector α has components unchanged under arbitrary reordering of its indices. Workers on symmetric cost models in Recognition Science cite it when proving equivalence between uniform weight vectors and those invariant under index permutation. The body is the direct predicate that α(σ i) equals α i for every permutation σ of Fin n and every index i.
Claim. Let α : ℝⁿ be a function from {0,…,n−1} to ℝ. Then α satisfies coefficient permutation invariance when α(σ(i)) = α(i) for every permutation σ of {0,…,n−1} and every index i.
background
The module treats permutation symmetry of coefficient weights in the N-dimensional cost setting. Vec n is defined as the type of functions Fin n → ℝ, supplying the coordinate representation for vectors that enter weighted dot products and logarithmic aggregates in the cost model. The definition sits immediately above the two equivalence theorems that link this invariance property to uniform weights.
proof idea
This is a definition whose body is the predicate ∀ σ : Equiv.Perm (Fin n), ∀ i : Fin n, α (σ i) = α i. No lemmas are applied; the statement itself encodes the invariance condition.
why it matters
The definition supplies the predicate used by coeff_perm_invariant_of_uniform and uniform_of_coeff_perm_invariant, which together establish logical equivalence between uniform weights and permutation-invariant coefficients. It thereby anchors the symmetry requirements imposed on coefficient vectors inside the N-dimensional cost calibration, consistent with the self-similar fixed-point and index-relabeling aspects of the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.