NP-Completeness of Deterministic Communication Complexity
Gaspers · He · Mackenzie — arXiv:2508.05597 · paper ⇄ Lean inspector
Scope of the machine check: Lean proves the choice-based threshold-gap equivalence, explicit and fixed-degree carrier/truth-table bounds in |V|+|E|+1, and square power-of-two padding preserving D, conditional on one balanced-family citation axiom. External: the bridge to chosen serialized source and target languages, executable construction/runtime, NP membership, and 4-Colouring hardness. Full audit · Citation boundary.