The six colours form the canonical type $Fin 6$, and a colouring is a plain function from vertices to colours. Properness is expressed directly by requiring adjacent vertices to have unequal images. This keeps the definition independent of decidability assumptions and equivalent to the usual assertion that the chromatic number is at most six, without introducing a separate chromatic-number parameter that no statement in this submission needs.

The definition applies to arbitrary vertex types because colourability is a pointwise graph property. The conjecture itself is stated on the canonical finite carriers $Fin n$.