Proof of `Independent Set Reduces to Multicoloured Clique` (13th statement)
groundedproofs/Lax496464Proofs/WHierarchy/MccNP/WordEncodesProof.lean · lax-496464
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The word encodes the construction. The word is the compressed sparse row block (the header , the prefix sums of the degrees, the concatenated increasing neighbour lists), the colours , and ; the block encodes the multicoloured graph, the length of the target array being even by the degree-sum formula, and each block is strictly increasing.