The graph is a mathlib $SimpleGraph (Fin n)$ and is encoded by the compressed sparse row format of $Lax271696.GraphEncoding$, so that an instance of this problem is an instance of the format every other statement in the archive built on that encoding uses. The colouring is appended as one entry per vertex, and the number of colours as a final entry, following the convention that a parameterized instance carries its parameter at the end of the word.

That adjacent vertices differ in colour is a field of the instance rather than a consequence: the source of this problem is a $k$-partite graph with edges only between distinct parts, and a reduction from it uses that the endpoints of an edge have two different colours. It costs nothing, since an instance violating it has no multicoloured clique through the offending edge anyway.

The adjacency list of each vertex is required to be strictly increasing. The archive's graph format does not ask for this — it lets a list name its neighbours in any order and more than once — but sorted lists are the convention of the format in practice, and the requirement is what lets a linear-time reduction enumerate the edges in a canonical order by a single scan. Without it a reduction would first have to sort and deduplicate its input; that is possible in linear time, but it is work about the input format rather than about the problem, and restricting the admissible words only makes the source problem easier to be reduced from in the sense that fewer words need handling — the problem itself, a graph and a colouring, is unchanged.

A solution is given as a function from colours to vertices rather than as a set, so that "one vertex of each colour" is the statement that the function is a section of the colouring, and the size of the clique needs no separate cardinality argument.