Fixed-vector rigidity

Transitivity of the label action forces fixed coordinate vectors to be constant. Intersecting this fixed subspace with the zero-sum representation leaves only the origin.

theorem NRR.PrimeSymmetry.coordinate_fixed_constant {p : ℕ} (hp : Nat.Prime p) (v : Fin p → ℝ) (hfix : ∀ (g : ↥(PrimeSymmetry p)), g • v = v) (i j : Fin p) : v i = v j

theorem NRR.PrimeSymmetry.coordinate_fixed_iff_constant {p : ℕ} (hp : Nat.Prime p) (v : Fin p → ℝ) : (∀ (g : ↥(PrimeSymmetry p)), g • v = v) ↔ ∃ (c : ℝ), v = fun (x : Fin p) => c

theorem NRR.PrimeSymmetry.zeroSum_fixed_eq_zero {p : ℕ} (hp : Nat.Prime p) (v : ZeroSum p) (hfix : ∀ (g : ↥(PrimeSymmetry p)), g • v = v) : v = 0

theorem NRR.coordinateMean_prime_smul (p : ℕ) (v : Fin p → ℝ) (g : ↥(PrimeSymmetry p)) : (coordinateMean p) (g • v) = (coordinateMean p) v

theorem NRR.coordinateDeviation_prime_smul {p : ℕ} (hp : Nat.Prime p) (v : Fin p → ℝ) (g : ↥(PrimeSymmetry p)) : (coordinateDeviation ⋯) (g • v) = g • (coordinateDeviation ⋯) v