Proof of `Independent Set Reduces to Multicoloured Clique` (13th statement)

groundedproofs/Lax496464Proofs/WHierarchy/MccNP/WordEncodesProof.lean · lax-496464

What this proof establishes

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

The word encodes the construction. The word is the compressed sparse row block (the header [N,M][N, M], the prefix sums of the degrees, the concatenated increasing neighbour lists), the colours ⌊s/n⌋⌊s / n⌋, and kk; 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.