coeff_perm_invariant_of_uniform
plain-language theorem explainer
Uniform real vectors satisfy permutation invariance of their coefficients. Researchers modeling symmetric cost functions in the N-dimensional Recognition Science framework cite this to confirm that equal-weight assignments meet the invariance requirement. The proof destructures the uniform hypothesis to a constant value and applies direct equality simplification.
Claim. Let $n$ be a natural number and let $α : ℝ^n$ be a vector. If there exists a real number $a$ such that $α_i = a$ for every index $i$, then $α(σ(i)) = α(i)$ for every permutation $σ$ of the indices and every index $i$.
background
The Cost.Ndim.Symmetry module treats permutation symmetry of coefficient weights. UniformWeights asserts that a vector $α$ (of type Vec n, i.e., a function from Fin n to ℝ) takes the same real value $a$ at every coordinate. CoeffPermutationInvariant requires that $α$ is unchanged when its indices are reordered by any permutation $σ$ in Equiv.Perm (Fin n). The result sits inside the cost domain and imports the uniform-weights definition from the Calibration submodule.
proof idea
One-line term proof that destructures the uniform-weights hypothesis into the constant $a$ and the pointwise equality $ha$. It then introduces an arbitrary permutation $σ$ and index $i$, after which simplification with $ha$ yields the required equality $α(σ i) = α i$.
why it matters
The declaration shows that the uniform case satisfies the permutation-invariance property needed for symmetric coefficient structures in the N-dimensional cost model. It supplies a basic instance of CoeffPermutationInvariant that can be used when constructing cost functions invariant under index reordering. No downstream applications are recorded yet; the result remains local to the symmetry submodule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.