The canonical colouring of multiset data

A multiset of even colours and a set of odd colours assemble into a canonical colouring: sorted even colours first, sorted odd colours after. This is the representative through which the vertex functional of Definition 5 evaluates the symmetric star coordinates.

noncomputable def RS.canonColouring {k ℓ : ℕ} (μm : Multiset (Fin k)) (F : Finset (Fin (2 * ℓ))) : MixedColouring k ℓ (μm.card + F.card)

The canonical colouring: sorted even colours, then sorted odd colours.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.canonColouring_isRight_low {k ℓ : ℕ} (μm : Multiset (Fin k)) (F : Finset (Fin (2 * ℓ))) (i : Fin (μm.card + F.card)) (h : ↑i < μm.card) : (canonColouring μm F i).isRight = false

Low positions are even colours.

theorem RS.canonColouring_isRight_high {k ℓ : ℕ} (μm : Multiset (Fin k)) (F : Finset (Fin (2 * ℓ))) (i : Fin (μm.card + F.card)) (h : ¬↑i < μm.card) : (canonColouring μm F i).isRight = true

High positions are odd colours.