Vector like charges

For the n-even case we define the property of a charge assignment being vector like.

theorem PureU1.split_equal (n : ℕ) : n + n = 2 * n

Given a natural number n, this lemma proves that n + n is equal to 2 * n.

theorem PureU1.split_odd (n : ℕ) : n + 1 + n = 2 * n + 1

def PureU1.VectorLikeEven {n : ℕ} (S : (PureU1 (2 * n)).Charges) : Prop

A charge configuration for n even is vector like if when sorted the ith element is equal to the negative of the n + ith element.

Equations

• PureU1.VectorLikeEven S = ∀ (i : Fin n), PureU1.sort S (Fin.cast ⋯ (Fin.castAdd n i)) = -PureU1.sort S (Fin.cast ⋯ (Fin.natAdd n i))