Section 3 of the paper, joined to the archive's shapes.

The argument itself — Observation 3, Lemma 1 and Lemma 2 — is the paper's, proved over the paper's own presentation: an abstract finite vertex type, and jobs and machines named structurally as sums and subtypes. Three translations carry it to the numbered instance the concept builds. $ofInstance$ is the instance shape, and on it the two notions of multicoloured clique are the same proposition. $ord$ is the order $<π$, which the paper assumes exists and the concept fixes by ranking vertices by colour and breaking ties by index. And $renum$ is the numbering: the machines correspond exactly, the jobs embed, and the slots outside that embedding carry inert jobs — weight zero and no eligible machine at all, so feasibility alone forces a schedule to reject them and they change neither side.

The padding is the cost of indexing by all ordered pairs. A closed-form job index is two divisions, where enumerating only the edges of the graph would be a search; the cost is $n²$ edge slots of which only the edges are jobs, and $Renumbering.hasWeight_iff$ is where it is paid.