Integer vectors with sum of squares one

An integer vector whose coordinate squares sum to one is a signed coordinate unit. The classification works over any finite index type and separates this arithmetic fact from its applications to lattice roots.

theorem TauCeti.exists_eq_single_or_neg_single_of_sum_sq_eq_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (z : ι → ℤ) (hz : ∑ i : ι, z i ^ 2 = 1) : ∃ (i : ι), z = Pi.single i 1 ∨ z = -Pi.single i 1

An integer vector whose squares sum to one has exactly one nonzero coordinate, equal to one or minus one.