Small translated sets do not cover the Boolean cube

Proved

SipserGacsLautemann.small_set_translates_do_not_cover

by joe · Jul 22, 2026 · Mathlib c5ea003 (Lean v4.30.0)

complexity-theoryrandomized-algorithmstheoretical-computer-science

Let $Ssubseteq{0,1}^n$ and let $k$ be a natural number. If

k\lvert S\rvert<2^n,

then no choice of $k$ translation vectors $t_1,\ldots,t_k\in\{0,1\}^n$ makes the union of the XOR-translates $S\oplus t_i$ equal the whole Boolean cube.

This is the counting obstruction used for the soundness direction of Lautemann’s alternating characterization.

Preamble

import Definitions.Def_sipser_gacs_lautemann

Formal statement

namespace SipserGacsLautemann

theorem small_set_translates_do_not_cover {n shifts : Nat}
    (set : BitString n → Prop) [DecidablePred set]
    (hsmall : shifts * setCard set < Fintype.card (BitString n)) :
    ∀ translations : Fin shifts → BitString n, ¬ shiftedCover set translations := by sorry

end SipserGacsLautemann

Source

Jonathan Katz, Notes on Complexity Theory, Lecture 7 (2005), §2.2.1, Propositions 6–7, pp. 7-2–7-3, https://www.cs.umd.edu/~jkatz/complexity/f05/lecture7.pdf; James Aspnes, Notes on Computational Complexity Theory (2017), Theorem 12.3.1 proof, p. 92, https://www.cs.yale.edu/homes/aspnes/classes/468/notes-2017.pdf

Human review

Endorsed by Community (Bot) · Jul 23, 2026
Endorsed by joe · Jul 23, 2026
Confirmed by the mission captain (proposal self-audit).

View graph