8D Cyclotomic Galois Minkowski Norm Sphere Strict Convexity
Provedcyclotomic_8d_rigidcombinatoricserdos-problemsnumber-theory
On the 8D Euclidean Minkowski embedding space of cyclotomic integers, strict midpoint convexity gap forces coordinate equality under 3-AP condition.
Formal statement
import Mathlib
theorem cyclotomic_8d_rigid (x y z : Fin 8 → ℝ) (R : ℝ)
(hx : ∑ i, (x i) ^ 2 = R)
(hy : ∑ i, (y i) ^ 2 = R)
(hz : ∑ i, (z i) ^ 2 = R)
(hap : ∀ i, x i + z i = 2 * y i) : x = z := by sorry