uniform_of_coeff_perm_invariant
plain-language theorem explainer
If a coefficient vector is invariant under arbitrary permutations of its indices, then all entries must be identical. Researchers modeling symmetric cost functions in Recognition Science cite this to collapse general coefficient assignments to uniform weights before calibration. The term proof fixes the zeroth index and applies the invariance hypothesis to the transposition swapping that index with any other.
Claim. Let $n$ be a positive integer and let $α : Fin n → ℝ$ satisfy $α(σ(i)) = α(i)$ for every permutation $σ$ of the indices and every index $i$. Then there exists a real number $a$ such that $α(i) = a$ for all $i$.
background
The module isolates permutation symmetry properties of coefficient weights inside n-dimensional cost vectors. Vec n is the type of n-component real vectors, realized as maps from Fin n to ℝ. CoeffPermutationInvariant α asserts that α is unchanged when its arguments are permuted by any element of the symmetric group on n elements. UniformWeights α asserts that α is constant, i.e., there exists a real a such that α(i) equals a for every index i.
proof idea
The proof is a direct term-mode construction. It selects the base index i0 := 0 (justified by hn : 0 < n). It exhibits the candidate constant value α i0 and, for arbitrary i, applies the invariance hypothesis to the transposition Equiv.swap i0 i evaluated at i0, which immediately yields α i = α i0.
why it matters
The result supplies the basic symmetry reduction from permutation invariance to uniformity for coefficient vectors in the cost model. It closes a prerequisite step presupposed by calibration routines in the sibling Calibration module, even though no immediate downstream uses are recorded in the current dependency graph. The equivalence aligns with Recognition Science practice of eliminating degrees of freedom via symmetry before extracting dimension-specific constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.