Two-position basis vectors, raw form

The colour-model basis vectors at two positions in the raw tensor structure (superPow V 1) ⊗ V: nested unit-padded standard basis vectors, one lemma per parity pattern.

theorem RS.evenSplitD_inl {k ℓ d : ℕ} (c : MixedColouring k ℓ (d + 1)) (hc : c.IsEven) (i : Fin k) (hi : c (Fin.last d) = Sum.inl i) : (evenSplitEquiv k ℓ d) ⟨c, hc⟩ = Sum.inl (⟨c.tail, ⋯⟩, i)

The forward even split, even last colour.

theorem RS.evenSplitD_inr {k ℓ d : ℕ} (c : MixedColouring k ℓ (d + 1)) (hc : c.IsEven) (b : Fin (2 * ℓ)) (hb : c (Fin.last d) = Sum.inr b) : (evenSplitEquiv k ℓ d) ⟨c, hc⟩ = Sum.inr (⟨c.tail, ⋯⟩, b)

The forward even split, odd last colour.

theorem RS.oddSplitD_inr {k ℓ d : ℕ} (c : MixedColouring k ℓ (d + 1)) (hc : ¬c.IsEven) (b : Fin (2 * ℓ)) (hb : c (Fin.last d) = Sum.inr b) : (oddSplitEquiv k ℓ d) ⟨c, hc⟩ = Sum.inr (⟨c.tail, ⋯⟩, b)

The forward odd split, odd last colour.

theorem RS.oddSplitD_inl {k ℓ d : ℕ} (c : MixedColouring k ℓ (d + 1)) (hc : ¬c.IsEven) (i : Fin k) (hi : c (Fin.last d) = Sum.inl i) : (oddSplitEquiv k ℓ d) ⟨c, hc⟩ = Sum.inl (⟨c.tail, ⋯⟩, i)

The forward odd split, even last colour.