Anti-checkers

An anti-checker for a Boolean function f against a family F of Boolean functions is a set S of inputs such that every member of F differs from f somewhere on S (IsAntiChecker) [LY94], [OliveiraPichSanthanam2019, Section 4]. Against the functions with circuits of at most s gates, S is an anti-checker for f exactly when f needs more than s gates on S (isAntiChecker_computableFunctions_iff), that is, when the Succinct MCSP instance of the values of f on S with threshold s is a no-instance.

Functions without small circuits have small anti-checkers. The combinatorial core is the good-string lemma of Oliveira, Pich and Santhanam [OliveiraPichSanthanam2019, Lemma 4.7]. Suppose the inputs number at most 2 ^ m, and no m members of F, repetitions allowed, have f as their pointwise strict majority. Then every tuple of m members of a subfamily G is refuted by at least half of its entries (at least m - m / 2 of them) at some input; averaging over the inputs, one input refutes a 2 ^ -m share of all tuples, and counting the tuples with at least half of their entries in the set of members refuted there shows that this set holds a sixteenth of G (exists_card_le_sixteen_mul). Removing the refuted members and repeating, 16 b inputs refute every member of a family of fewer than 2 ^ b (exists_isAntiChecker). Counting ordered tuples gives the constant share 1 / 16 where the original counts sets and gets 1 / (2 m).

For circuits (exists_lt_complexityOn): the strict majority of m circuits with s gates each has a circuit with m s gates plus those of a circuit for strict majority, so if f needs more than that, then f needs more than s gates on some set of 16 b inputs, for any b with fewer than 2 ^ b functions computable with s gates.

This is the existence of anti-checkers: the worst-case form of the theorem of Lipton and Young, with the combinatorial proof of Oliveira, Pich and Santhanam. Their Anti-Checker Lemma, which computes an anti-checker from the truth table by a small circuit if NP ⊆ P/poly, is not formalized here.

Main definitions

• Cslib.MCSP.IsAntiChecker: anti-checkers against a family of Boolean functions.

Main results

• Cslib.MCSP.exists_card_le_sixteen_mul: the good-string lemma.
• Cslib.MCSP.exists_isAntiChecker: small anti-checkers, combinatorially.
• Cslib.MCSP.isAntiChecker_computableFunctions_iff, Cslib.MCSP.isAntiChecker_computableFunctions_iff_not_mem: anti-checkers against circuits.
• Cslib.MCSP.exists_lt_complexityOn, Cslib.MCSP.exists_ofFunction_not_mem: small anti-checkers against circuits.

References

• R. J. Lipton, N. E. Young, Simple strategies for large zero-sum games with applications to complexity theory
• I. C. Oliveira, J. Pich, R. Santhanam, Hardness magnification near state-of-the-art lower bounds

def Cslib.MCSP.IsAntiChecker {α : Type u_1} (F : Set (α → Bool)) (f : α → Bool) (S : Set α) : Prop

S is an anti-checker for f against the family F: every member of F differs from f at some input in S.

Counting refuting tuples

theorem Cslib.MCSP.exists_card_le_sixteen_mul {α : Type u_1} [Fintype α] {m : ℕ} (hm : 0 < m) (hα : Fintype.card α ≤ 2 ^ m) {G : Finset (α → Bool)} (hG : G.Nonempty) {f : α → Bool} (hmaj : ∀ (g : Fin m → α → Bool), (∀ (i : Fin m), g i ∈ G) → (fun (x : α) => strictMajority m fun (i : Fin m) => g i x) ≠ f) : ∃ (x : α), G.card ≤ 16 * {g ∈ G | g x ≠ f x}.card

The good-string lemma [OliveiraPichSanthanam2019, Lemma 4.7]. Suppose there are at most 2 ^ m inputs and no m members of the nonempty family G have f as their pointwise strict majority. Then at some input x, at least a sixteenth of the members of G differ from f.

Small anti-checkers

theorem Cslib.MCSP.exists_isAntiChecker {α : Type u_1} [Fintype α] {m b : ℕ} (hm : 0 < m) (hα : Fintype.card α ≤ 2 ^ m) (F : Finset (α → Bool)) {f : α → Bool} (hmaj : ∀ (g : Fin m → α → Bool), (∀ (i : Fin m), g i ∈ F) → (fun (x : α) => strictMajority m fun (i : Fin m) => g i x) ≠ f) (hb : F.card < 2 ^ b) : ∃ (S : Finset α), S.card ≤ 16 * b ∧ IsAntiChecker (↑F) f ↑S

Small anti-checkers, combinatorially [OliveiraPichSanthanam2019, Lemma 4.7]. Suppose there are at most 2 ^ m inputs, with m > 0, and no m members of F, repetitions allowed, have f as their pointwise strict majority. If F has fewer than 2 ^ b members, some set of at most 16 b inputs is an anti-checker for f against F.

Anti-checkers against circuits

theorem Cslib.MCSP.isAntiChecker_computableFunctions_iff {n s : ℕ} {f : BooleanFunction n} {S : Set (BitString n)} : IsAntiChecker (↑(Circuits.Boolean.computableFunctions n s)) f S ↔ s < Circuits.complexityOn Circuits.Boolean.interpretation S (Circuits.single f)

Against the functions computable with at most s gates, S is an anti-checker for f exactly when f needs more than s gates on S.

theorem Cslib.MCSP.isAntiChecker_computableFunctions_iff_not_mem {n s : ℕ} {f : BooleanFunction n} {S : Finset (BitString n)} : IsAntiChecker (↑(Circuits.Boolean.computableFunctions n s)) f ↑S ↔ SuccinctMCSP.Instance.ofFunction f S s ∉ SuccinctMCSP

Against the functions computable with at most s gates, S is an anti-checker for f exactly when the Succinct MCSP instance of the values of f on S, with threshold s, is a no-instance.

theorem Cslib.MCSP.exists_lt_complexityOn {n s m b : ℕ} (hm : 0 < m) (hnm : n ≤ m) {f : BooleanFunction n} (hf : m * s + Circuits.complexity Circuits.Boolean.interpretation (Circuits.single (strictMajority m)) < Circuits.complexity Circuits.Boolean.interpretation (Circuits.single f)) (hb : (Circuits.Boolean.computableFunctions n s).card < 2 ^ b) : ∃ (S : Finset (BitString n)), S.card ≤ 16 * b ∧ s < Circuits.complexityOn Circuits.Boolean.interpretation (↑S) (Circuits.single f)

Small anti-checkers against circuits [OliveiraPichSanthanam2019, Lemma 4.7]. Let n ≤ m with m > 0. If f needs more than m s gates plus the complexity of strict majority on m bits, and fewer than 2 ^ b functions on n inputs have circuits with at most s gates, then on some set of at most 16 b inputs f needs more than s gates.

theorem Cslib.MCSP.exists_ofFunction_not_mem {n s m b : ℕ} (hm : 0 < m) (hnm : n ≤ m) {f : BooleanFunction n} (hf : m * s + Circuits.complexity Circuits.Boolean.interpretation (Circuits.single (strictMajority m)) < Circuits.complexity Circuits.Boolean.interpretation (Circuits.single f)) (hb : (Circuits.Boolean.computableFunctions n s).card < 2 ^ b) : ∃ (S : Finset (BitString n)), S.card ≤ 16 * b ∧ SuccinctMCSP.Instance.ofFunction f S s ∉ SuccinctMCSP

Small anti-checkers against circuits, as Succinct MCSP: under the hypotheses of exists_lt_complexityOn, the values of f on some set of at most 16 b inputs are a no-instance of Succinct MCSP at threshold s.