Formula Magnification for Succinct, Partial, and Approximate MCSP

This module formalizes the De Morgan formula hardness magnification results of Oliveira and Santhanam [OS18]:

• Lemma 16 ([OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]): the two-stage magnification lemma connecting Cslib.SuccinctMCSP and Cslib.PartialMCSP to approximate MCSP (Cslib.ApproxMCSP, corresponding to (1, 1 - δ)-MCSP[s] in [OliveiraSanthanam2018, Appendix A, Definition 41, p. 34]) and Cslib.GapMCSP.
• Contrapositive of Lemma 16 and Theorem 1(i) / Theorem 17(i) ([OliveiraSanthanam2018, Section 1.2, Theorem 1 (i), p. 5; Section 3.1, Lemma 16 and Theorem 17 (i), pp. 14–15]): packaging Lemma 16 with SuccinctMCSP ∈ NP (Cslib.SuccinctMCSP.mem_NP) into SuccinctMCSP ∉ FormulaPolyOn SuccinctMCSP.enc and NP SuccinctMCSP.enc ⊄ FormulaPolyOn SuccinctMCSP.enc (NP ⊄ Formula[poly]), both in the general-parameter form underlying Theorem 17(i)/(iii) and specialized to polynomially bounded parameters s₂, k for Theorem 1(i) / Theorem 17(i).
• Lemma 26 and one-sided Theorem 27 ([OliveiraSanthanam2018, Section 3.3, Lemma 26 and Theorem 27, p. 21]; compare [OliveiraSanthanam2018, Section 1.2, Theorem 5, p. 8]): deterministic counting form of Lemma 26 and one-sided zero-error average-case De Morgan formula magnification from MCSP[s] to SuccinctMCSP and NP ⊄ FormulaPolyOn.

Source Statements (ECCC TR18-139)

Verbatim from [OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]:

Lemma 16 (Magnification Lemma for Formulas). Let s : ℕ → ℕ and δ : ℕ → [0, 1/2) be constructive functions, where s(n) ≥ n. Consider the promise problem Π[s, δ] = (1, 1 − δ)-MCSP[s], where for every N = 2ⁿ, Π^yes_N = {y ∈ {0,1}^N | ∃ circuit of size ≤ s(n) that computes fn(y)}, Π^no_N = {y ∈ {0,1}^N | ∄ circuit of size ≤ s(n) that (1 − δ(n))-approximates fn(y)}. Then, for every function ℓ : ℕ → ℕ, if Π[s, δ] cannot be computed by formulas of size N · ℓ(n), then there is a sequence {f_{m(n)}}_{n≥1} of m(n)-bit functions in NP that cannot be computed by formulas of size ≤ ℓ(n), where m(n) = Θ((n · s(n) · log s(n))/δ(n)).

Verbatim from [OliveiraSanthanam2018, Section 3.1, Theorem 17, p. 15] (also stated as [OliveiraSanthanam2018, Section 1.2, Theorem 1, pp. 5–6], with proof "Immediate from Lemma 16."):

Theorem 17 (Magnification of Weak Formula Lower Bounds). For convenience, let Π[s, δ] = (1, 1 − δ)-MCSP[s]. The following implications hold. (i) Let s(n) = n^k and δ(n) = n^{−k}, where k ∈ ℕ. If Π[s, δ] ∉ Formula[N · (log N)^{O(1)}] then there is L ∈ NP over m-bit inputs such that L ∉ Formula[poly(m)]. (ii) For the same choice of parameters, if Π[s, δ] ∉ Formula[N^{1+ε}] for some ε > 0, then there is L ∈ NP over m-bit inputs and δ > 0 such that L ∉ Formula[2^{m^δ}]. (iii) Let s(n) = 2^{o(n)} and δ(n) = 2^{−o(n)}. If Π[s, δ] ∉ Formula[N^{1+ε}] for some ε > 0, then there is L ∈ NP over m-bit inputs such that L ∉ Formula[poly(m)].

Verbatim from [OliveiraSanthanam2018, Section 1.2, Theorem 5, p. 8], [OliveiraSanthanam2018, Section 3.3, Lemma 26 and Theorem 27, p. 21], and [OliveiraSanthanam2018, Appendix A, Definition 43, p. 34]:

Theorem 5. If MCSP[2^{√n}] on N-bit inputs cannot be solved on average with zero error by formulas of size o(N), then NP does not have polynomial size formulas.

Lemma 26. Let n ≤ s(n) ≤ 2^{o(n)} and t(n) = 4s(n) log s(n). Let I be a random collection of t(n) pairs of the form (x_i, b_i), where each b_i ∼ {0, 1}, and all x_i are fixed but distinct elements of {0, 1}^n. Then, for every n sufficiently large, Pr_I[ There is a circuit of size ≤ s(n) consistent with I ] < 2^{−n}.

Theorem 27 (Magnification from sub-linear average-case lower bounds for MCSP). Let C be a typical circuit class, and consider MCSP[s] for a size parameter n ≤ s(n) ≤ 2^{o(n)}. Assume that there exists δ > 0 such that solving MCSP[s] on average on N-bit inputs requires C-circuits of size Ω(N^δ). Then there is a language L in NP such that L on inputs of length m = Θ(n · s(n) · log s(n)) requires C-circuits of size ℓ(m) = 2^{Ω(n)}.

Definition 43 (Average-case MCSP [HS17]). We say that MCSP-C[s] is computed on average by a device D (an algorithm or a family of circuits) if for every large enough n, the following holds: • D is never incorrect. For each y ∈ {0, 1}^{2^n}, D(y) ∈ {MCSP-C[s](y), “?”}. • D rarely outputs “?”. Pr_{z∼{0,1}^{2^n}}[D(z) ∈ {0, 1}] ≥ 1 − 1/n. We say that MCSP-C[s] is average-case hard for a class of devices A if no D ∈ A computes MCSP-C[s] on average.

Here [OliveiraSanthanam2018, Appendix A, Definition 41, p. 34] defines (α, β)-MCSP[s] for α, β ∈ (1/2, 1] using "γ-approximates" to mean Pr_x[ψ(x) = f(x)] ≥ γ, so (1, 1 - δ)-MCSP[s] is the α = 1, β = 1 - δ specialization. For average-case MCSP, Section 1.2 (p. 8) discusses zero-error average-case algorithms informally (never wrong, Pr[A(x) = ?] ≤ 1/2), Definition 43 (Appendix A, p. 34) formalizes three-valued devices D(y) ∈ {MCSP-C[s](y), "?"} with Pr_z[D(z) ∈ {0, 1}] ≥ 1 - 1/n, and the proof of Theorem 27 (Section 3.3, p. 21) constructs such a device C_n from a {0, 1}-valued circuit D_m for Succinct-MCSP[s, t] by outputting 0 when D_m outputs 0 and "?" otherwise. Our Lean hypotheses (exists_formula_zero_error_average_case_of_sample, not_NP_subset_FormulaPolyOn_of_zero_error_average_case_hard) are stated directly in terms of these one-sided {0, 1}-valued formulas F (accepting all yes-instances in GapMCSP.yesSet s and accepting at most 2 ^ (2 ^ n - r) truth tables overall): any three-valued Definition 43 device D induces the one-sided predicate F(T) = decide (D(T) ≠ 0) with r = 1 once 1/n plus the yes-instance fraction is at most 1/2, modulo the formula encoding of three-valued outputs.

Comparison Between ECCC TR18-139 and This Module

1. Circuit-Size Thresholds (s vs. s₁ ≤ s₂): ECCC Lemma 16 and Theorem 17 use a single circuit-size threshold s(n) for both Π^yes_N and Π^no_N. Here we allow distinct yes/no thresholds s₁ n ≤ s₂ n (s₁ = s₂ = s recovers the source setting).
2. Error Parameter (δ(n) ∈ [0, 1/2) vs. 1 / k n with 1 ≤ k n): ECCC Lemma 16 takes a real-valued function δ : ℕ → [0, 1/2). In the end-to-end theorems we parameterize the error by an integer function k : ℕ → ℕ with 1 ≤ k n corresponding to δ(n) = 1 / k n (and also provide the real-parameter Stage 2 amplification exists_seed_tuple_of_one_sided_error_real and exists_formula_separating_gapMCSP_of_succinctMCSP_real using ⌈1 / δ⌉₊).
3. Strict vs. Non-Strict No-Instances: In ECCC Definition 41 (Appendix A, p. 34), "(1 - δ(n))- approximates" means agreement on at least (1 - δ(n)) ⋅ 2^n inputs, so Π^no_N requires every circuit of size ≤ s(n) to agree with fn(y) on strictly fewer than (1 - δ(n)) ⋅ 2^n inputs. Here ApproxMCSP.noSet s₂ k requires k n * card(Agree) ≤ (k n - 1) * 2 ^ n (non-strict ≤), which contains the strict no-set, making the separation and contrapositive magnification theorems at least as strong.
4. Target Representation (Succinct-Π[s, t] vs. Finset Samples in SuccinctMCSP): The proof of ECCC Lemma 16 (p. 14) reduces Π[s, δ] to Succinct-Π[s, t], an explicit Succinct-MCSP encoding of t(n) = 3 s(n) log s(n) / δ(n) input-output samples (with possible repetition). Here SuccinctMCSP.Instance.ofFunction deduplicates a Finset (BitString n) sample S into a canonical sorted list of m = S.card samples of exact encoded length SuccinctMCSP.ofFunctionEncLength n m (s₂ n) = 4 * n + 3 + m * (8 * n + 10) + s₂ n. Because deduplicating q = k n * (M + 2) independent samples ω : Fin q → BitString n into Finset.univ.image ω can have any cardinality m ≤ k n * (M + 2), our end-to-end theorems quantify over m ≤ k n * (M + 2) (with maximum encoded length approxMCSPQueryEncLength). We also provide exists_formula_separating_gapMCSP_of_partialMCSP bridging to Cslib.PartialMCSP.Instance.restrictTable.
5. Circuit Model and Counting Bound (s^{O(s)} vs. computableFunctionsLogBound): ECCC Lemma 16 and Lemma 26 count fan-in-two Boolean circuits of size at most s(n). Here small functions are computableFunctions n s (defined via Cslib.Circuits.complexity interpretation), and card_computableFunctions_le_two_pow bounds (computableFunctions n s).card ≤ 2 ^ M with M = computableFunctionsLogBound n s = (s + 1) * (2 * Nat.clog 2 (n + s + 1) + 3) from Cslib.Circuits.Boolean.card_computableFunctions_mul_factorial_le.
6. Conclusion (FormulaPolyOn and NP ⊄ FormulaPolyOn in Theorem 1/17 and Theorem 5/27): Generalizing the word-level formula projection (exists_formula_ofFunction_SuccinctMCSP_of_agrees) to any language L : Language Bool agreeing with SuccinctMCSP along SuccinctMCSP.enc connects Lemma 16 and Theorem 27 directly to FormulaSIZEOn SuccinctMCSP.enc and FormulaPolyOn SuccinctMCSP.enc (Complexity.Computability.Circuit.Boolean.Formula.Poly). Combining with SuccinctMCSP.mem_NP yields both the general-parameter magnification to NP SuccinctMCSP.enc ⊄ FormulaPolyOn SuccinctMCSP.enc (not_NP_subset_FormulaPolyOn_of_approxMCSP_hard) and the polynomially-bounded-parameter N · (log N)^{O(1)} magnification (not_NP_subset_FormulaPolyOn_of_approxMCSP_poly_hard, matching Theorem 1(i) / Theorem 17(i)), as well as the zero-error average-case magnification (not_NP_subset_FormulaPolyOn_of_zero_error_average_case_hard, matching Lemma 26 and Theorem 5 / Theorem 27).

Main definitions

• Cslib.Circuits.Boolean.evalWord, Cslib.Circuits.Boolean.succinctWord: word-level formula projections for SuccinctMCSP.enc.
• Cslib.ApproxMCSP.noSet, Cslib.ApproxMCSP: the approximate (1, 1 - 1 / k)-MCSP promise problem [OliveiraSanthanam2018, Appendix A, Definition 41, p. 34].
• Cslib.Circuits.Boolean.computableFunctionsLogBound: explicit s log(n + s) exponent bound (s + 1) * (2 * Nat.clog 2 (n + s + 1) + 3) for (computableFunctions n s).card.
• Cslib.Circuits.Boolean.approxMCSPQueryEncLength, Cslib.Circuits.Boolean.avgCaseMCSPQueryEncLength: encoded query lengths for the worst-case (Lemma 16 / Theorem 17) and zero-error average-case (Lemma 26 / Theorem 27) reductions.

Main results

• Cslib.Circuits.Boolean.evalWord_succinctWord, Cslib.Circuits.Boolean.leafSize_le_one_of_mem_succinctWord, Cslib.Circuits.Boolean.exists_formula_ofFunction_SuccinctMCSP_of_agrees, Cslib.Circuits.Boolean.exists_formula_ofFunction_SuccinctMCSP: leaf-size-preserving substitution into a slice formula of SuccinctMCSP.
• Cslib.Circuits.Boolean.exists_formula_all_ofFunction_SuccinctMCSP_of_agrees, Cslib.Circuits.Boolean.exists_formula_all_ofFunction_SuccinctMCSP, Cslib.Circuits.Boolean.exists_formula_separating_gapMCSP_of_queryList, Cslib.Circuits.Boolean.exists_mem_lt_formulaSize_succinctMCSP_of_queryList: deterministic multi-query formula projection (building block for [OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]).
• Cslib.Circuits.Boolean.two_pow_mul_pred_pow_lt, Cslib.Circuits.Boolean.exists_seed_tuple_of_one_sided_error, Cslib.Circuits.Boolean.exists_seed_tuple_of_one_sided_error_real: finite-probability Adleman derandomization lemma from Cslib.exists_cover_of_scaled_card_lt.
• Cslib.Circuits.Boolean.exists_formula_separating_gapMCSP_of_succinctMCSP, Cslib.Circuits.Boolean.exists_formula_separating_gapMCSP_of_succinctMCSP_real, Cslib.Circuits.Boolean.exists_lt_formulaSize_succinctMCSP_of_gapMCSP, Cslib.Circuits.Boolean.exists_formula_separating_gapMCSP_of_partialMCSP: Stage 2 derandomization of an assumed one-sided sample projection ([OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]).
• Cslib.Circuits.Boolean.card_computableFunctions_le_two_pow, Cslib.Circuits.Boolean.card_le_two_mul_filter_notMem_succinctMCSP, Cslib.Circuits.Boolean.exists_formula_separating_approxMCSP_of_succinctMCSP, Cslib.Circuits.Boolean.exists_lt_formulaSize_succinctMCSP_of_approxMCSP, Cslib.Circuits.Boolean.exists_formula_separating_approxMCSP_of_succinctMCSP_inst, Cslib.Circuits.Boolean.exists_lt_formulaSize_succinctMCSP_of_approxMCSP_inst: Stage 1 random sampling and end-to-end approximate (1, 1 - 1 / k)-MCSP formula magnification [OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14].
• Cslib.Circuits.Boolean.exists_formula_separating_approxMCSP_of_mem_FormulaSIZEOn, Cslib.Circuits.Boolean.not_succinctMCSP_mem_FormulaPolyOn_of_approxMCSP_hard, Cslib.Circuits.Boolean.not_NP_subset_FormulaPolyOn_of_approxMCSP_hard, Cslib.Circuits.Boolean.exists_poly_formula_separating_approxMCSP_of_mem_FormulaPolyOn, Cslib.Circuits.Boolean.not_succinctMCSP_mem_FormulaPolyOn_of_approxMCSP_poly_hard, Cslib.Circuits.Boolean.not_NP_subset_FormulaPolyOn_of_approxMCSP_poly_hard: packaging Lemma 16 with SuccinctMCSP.mem_NP into SuccinctMCSP ∉ FormulaPolyOn SuccinctMCSP.enc and NP ⊄ FormulaPolyOn (general-parameter contrapositive of Lemma 16 underlying Theorem 17(i)/(iii), and Theorem 1(i) / Theorem 17(i) for polynomially bounded parameters) [OliveiraSanthanam2018, Section 1.2, Theorem 1 (i), p. 5; Section 3.1, Lemma 16 and Theorem 17 (i), pp. 14–15].
• Cslib.Circuits.Boolean.card_filter_agreesOn_eq_two_pow, Cslib.Circuits.Boolean.card_filter_ofFunction_mem_succinctMCSP_le, Cslib.Circuits.Boolean.card_filter_ofFunction_mem_succinctMCSP_le_two_pow, Cslib.Circuits.Boolean.exists_formula_zero_error_average_case_of_sample, Cslib.Circuits.Boolean.exists_formula_zero_error_average_case_of_agrees, Cslib.Circuits.Boolean.exists_formula_zero_error_average_case_of_succinctMCSP, Cslib.Circuits.Boolean.lt_formulaSize_succinctMCSP_of_zero_error_average_case, Cslib.Circuits.Boolean.not_succinctMCSP_mem_FormulaPolyOn_of_zero_error_average_case_hard, Cslib.Circuits.Boolean.not_NP_subset_FormulaPolyOn_of_zero_error_average_case_hard: one-sided zero-error average-case formula magnification from MCSP[s] to SuccinctMCSP and NP ⊄ FormulaPolyOn [OliveiraSanthanam2018, Section 3.3, Lemma 26 and Theorem 27, p. 21; compare Section 1.2, Theorem 5, p. 8].

References

• I. C. Oliveira, R. Santhanam, Hardness Magnification for Natural Problems

Word-level projections by leaf-size-≤ 1 De Morgan formulas

def Cslib.Circuits.Boolean.evalWord {N : ℕ} (fs : List (Formula signature N)) (T : BitString N) : List Bool

Evaluate a list of De Morgan formulas on a bitstring T to produce a binary word.

@[simp]

theorem Cslib.Circuits.Boolean.evalWord_nil {N : ℕ} (T : BitString N) : evalWord [] T = []

@[simp]

theorem Cslib.Circuits.Boolean.evalWord_cons {N : ℕ} (F : Formula signature N) (fs : List (Formula signature N)) (T : BitString N) : evalWord (F :: fs) T = F.eval interpretation T :: evalWord fs T

@[simp]

theorem Cslib.Circuits.Boolean.evalWord_append {N : ℕ} (fs₁ fs₂ : List (Formula signature N)) (T : BitString N) : evalWord (fs₁ ++ fs₂) T = evalWord fs₁ T ++ evalWord fs₂ T

@[simp]

theorem Cslib.Circuits.Boolean.length_evalWord {N : ℕ} (fs : List (Formula signature N)) (T : BitString N) : (evalWord fs T).length = fs.length

def Cslib.Circuits.Boolean.constWord (N : ℕ) (w : List Bool) : List (Formula signature N)

A fixed binary word w lifted to a list of constant De Morgan formulas on N inputs.

@[simp]

theorem Cslib.Circuits.Boolean.evalWord_constWord {N : ℕ} (w : List Bool) (T : BitString N) : evalWord (constWord N w) T = w

def Cslib.Circuits.Boolean.frameWord {N : ℕ} (fs : List (Formula signature N)) : List (Formula signature N)

Lift Turing.MultiTapeTM.frame to a list of De Morgan formulas: each formula F becomes [Formula.const true, F], terminated by [Formula.const false].

@[simp]

theorem Cslib.Circuits.Boolean.evalWord_frameWord {N : ℕ} (fs : List (Formula signature N)) (T : BitString N) : evalWord (frameWord fs) T = Turing.MultiTapeTM.frame (evalWord fs T)

def Cslib.Circuits.Boolean.pairWord {N : ℕ} (fs₁ fs₂ : List (Formula signature N)) : List (Formula signature N)

Lift Turing.MultiTapeTM.encPair to two lists of De Morgan formulas.

@[simp]

theorem Cslib.Circuits.Boolean.evalWord_pairWord {N : ℕ} (fs₁ fs₂ : List (Formula signature N)) (T : BitString N) : evalWord (pairWord fs₁ fs₂) T = Turing.MultiTapeTM.frame (evalWord fs₁ T) ++ evalWord fs₂ T

def Cslib.Circuits.Boolean.sampleWord (n : ℕ) (y : BitString n) : List (Formula signature (2 ^ n))

The formula word on 2 ^ n variables encoding a single sample (List.ofFn y, f y) where f = (MCSP.truthTable n).symm T: the input bits List.ofFn y are constants and the output bit f y = T (BitString.equivFin n y) is a single input leaf.

@[simp]

theorem Cslib.Circuits.Boolean.evalWord_sampleWord (n : ℕ) (y : BitString n) (T : BitString (2 ^ n)) : evalWord (sampleWord n y) T = (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) (List.ofFn y, (MCSP.truthTable n).symm T y)

def Cslib.Circuits.Boolean.succinctWord (n : ℕ) (S : Finset (BitString n)) (s : ℕ) : List (Formula signature (2 ^ n))

The formula word on 2 ^ n variables whose evaluation on a truth table T equals SuccinctMCSP.enc (SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s).

@[simp]

theorem Cslib.Circuits.Boolean.evalWord_succinctWord (n : ℕ) (S : Finset (BitString n)) (s : ℕ) (T : BitString (2 ^ n)) : evalWord (succinctWord n S s) T = SuccinctMCSP.enc (SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s)

Evaluating succinctWord n S s on a truth table T : BitString (2 ^ n) produces the exact encoding SuccinctMCSP.enc (SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s).

theorem Cslib.Circuits.Boolean.leafSize_le_one_of_mem_succinctWord {n : ℕ} {S : Finset (BitString n)} {s : ℕ} {F : Formula signature (2 ^ n)} (hF : F ∈ succinctWord n S s) : F.leafSize ≤ 1

Every formula in succinctWord n S s has leaf size at most 1 (it is either a constant or a single input leaf).

@[simp]

theorem Cslib.Circuits.Boolean.length_succinctWord (n : ℕ) (S : Finset (BitString n)) (s : ℕ) : (succinctWord n S s).length = SuccinctMCSP.ofFunctionEncLength n S.card s

The length of succinctWord n S s is SuccinctMCSP.ofFunctionEncLength n S.card s.

theorem Cslib.Circuits.Boolean.exists_formula_of_evalWord {N : ℕ} (fs : List (Formula signature N)) (hfs : ∀ F ∈ fs, F.leafSize ≤ 1) (L : Set (List Bool)) : ∃ (F : Formula signature N), (∀ (T : BitString N), F.eval interpretation T = decide (evalWord fs T ∈ L)) ∧ F.leafSize ≤ formulaSize (Language.slice L fs.length)

Leaf-size-preserving substitution into a language slice. If every formula in fs : List (Formula signature N) has leaf size at most 1, then membership of evalWord fs T in any language L : Set (List Bool) is computed by a De Morgan formula on N variables of leaf size at most formulaSize (Language.slice L fs.length).

theorem Cslib.Circuits.Boolean.exists_formula_ofFunction_SuccinctMCSP_of_agrees {L : Language Bool} (hag : ∀ (x : SuccinctMCSP.Instance), x ∈ SuccinctMCSP ↔ SuccinctMCSP.enc x ∈ L) (n : ℕ) (S : Finset (BitString n)) (s : ℕ) : ∃ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), F.eval interpretation T = decide (SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s ∈ SuccinctMCSP)) ∧ F.leafSize ≤ formulaSize (L.slice (SuccinctMCSP.ofFunctionEncLength n S.card s))

Single-query SuccinctMCSP formula projection for any agreeing language. If L : Language Bool agrees with SuccinctMCSP along SuccinctMCSP.enc (∀ x, x ∈ SuccinctMCSP ↔ SuccinctMCSP.enc x ∈ L), then for any n, S : Finset (BitString n), and s, there is a De Morgan formula F on 2 ^ n variables that decides whether SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s ∈ SuccinctMCSP and has leaf size at most formulaSize (L.slice (SuccinctMCSP.ofFunctionEncLength n S.card s)).

theorem Cslib.Circuits.Boolean.exists_formula_ofFunction_SuccinctMCSP (n : ℕ) (S : Finset (BitString n)) (s : ℕ) : ∃ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), F.eval interpretation T = decide (SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s ∈ SuccinctMCSP)) ∧ F.leafSize ≤ formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (SuccinctMCSP.ofFunctionEncLength n S.card s))

Single-query SuccinctMCSP formula projection. For any n, S : Finset (BitString n), and s, there is a De Morgan formula F on 2 ^ n variables that decides whether SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s ∈ SuccinctMCSP and has leaf size at most the formula size of the (ofFunctionEncLength n S.card s)-bit slice of SuccinctMCSP.enc '' SuccinctMCSP.

Deterministic multi-query formula projection (building block for Stage 2)

theorem Cslib.Circuits.Boolean.exists_formula_all_ofFunction_SuccinctMCSP_of_agrees {L : Language Bool} (hag : ∀ (x : SuccinctMCSP.Instance), x ∈ SuccinctMCSP ↔ SuccinctMCSP.enc x ∈ L) (n : ℕ) (qs : List (Finset (BitString n) × ℕ)) : ∃ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), F.eval interpretation T = decide (∀ p ∈ qs, SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) p.1 p.2 ∈ SuccinctMCSP)) ∧ F.leafSize ≤ (List.map (fun (p : Finset (BitString n) × ℕ) => formulaSize (L.slice (SuccinctMCSP.ofFunctionEncLength n p.1.card p.2))) qs).sum

Multi-query SuccinctMCSP conjunction formula for any agreeing language. If L : Language Bool agrees with SuccinctMCSP along SuccinctMCSP.enc, then for any list qs : List (Finset (BitString n) × ℕ) of sample sets and thresholds, there is a De Morgan formula on 2 ^ n variables that decides whether all queries (S, s) ∈ qs are in SuccinctMCSP and has leaf size at most the sum of the corresponding slice formula sizes of L.

theorem Cslib.Circuits.Boolean.exists_formula_all_ofFunction_SuccinctMCSP (n : ℕ) (qs : List (Finset (BitString n) × ℕ)) : ∃ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), F.eval interpretation T = decide (∀ p ∈ qs, SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) p.1 p.2 ∈ SuccinctMCSP)) ∧ F.leafSize ≤ (List.map (fun (p : Finset (BitString n) × ℕ) => formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (SuccinctMCSP.ofFunctionEncLength n p.1.card p.2))) qs).sum

Multi-query SuccinctMCSP conjunction formula. Given any list qs : List (Finset (BitString n) × ℕ) of sample sets and thresholds, there is a De Morgan formula on 2 ^ n variables that decides whether all queries (S, s) ∈ qs are in SuccinctMCSP and has leaf size at most the sum of the corresponding slice formula sizes.

theorem Cslib.Circuits.Boolean.exists_formula_separating_gapMCSP_of_queryList {s₁ s₂ : ℕ → ℕ} {n L : ℕ} (qs : List (Finset (BitString n) × ℕ)) (hs : ∀ p ∈ qs, s₁ n ≤ p.2) (hno : ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.noSet s₂ → ∃ p ∈ qs, SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) p.1 p.2 ∉ SuccinctMCSP) (hL : ∀ p ∈ qs, formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (SuccinctMCSP.ofFunctionEncLength n p.1.card p.2)) ≤ L) : ∃ (F : Formula signature (2 ^ n)), F.leafSize ≤ qs.length * L ∧ (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) ∧ ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.noSet s₂ → F.eval interpretation T = false

Deterministic multi-query formula projection for GapMCSP (building block for [OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]). If a deterministic list qs of (S, s) queries has s₁ n ≤ s for every (S, s) ∈ qs and rejects every T ∈ GapMCSP.noSet s₂ on at least one query in qs, and each queried slice of SuccinctMCSP has formula size at most L, then GapMCSP[s₁, s₂] on 2 ^ n-bit inputs is separated by a De Morgan formula of leaf size at most qs.length * L.

theorem Cslib.Circuits.Boolean.exists_mem_lt_formulaSize_succinctMCSP_of_queryList {s₁ s₂ : ℕ → ℕ} {n L : ℕ} (qs : List (Finset (BitString n) × ℕ)) (hs : ∀ p ∈ qs, s₁ n ≤ p.2) (hno : ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.noSet s₂ → ∃ p ∈ qs, SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) p.1 p.2 ∉ SuccinctMCSP) (hged : ∀ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) → (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.noSet s₂ → F.eval interpretation T = false) → qs.length * L < F.leafSize) : ∃ p ∈ qs, L < formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (SuccinctMCSP.ofFunctionEncLength n p.1.card p.2))

Contrapositive deterministic multi-query formula projection (building block for [OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]). If every De Morgan formula separating GapMCSP.yesSet s₁ and GapMCSP.noSet s₂ on 2 ^ n-bit inputs has leaf size strictly greater than qs.length * L, then at least one query p ∈ qs maps to a slice of SuccinctMCSP with formula size strictly greater than L.

theorem Cslib.Circuits.Boolean.formulaSize_slice_yesSet_le (s : ℕ → ℕ) (n : ℕ) : formulaSize ((GapMCSP.yesSet s).slice (2 ^ n)) ≤ formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (SuccinctMCSP.ofFunctionEncLength n (2 ^ n) (s n)))

Querying the full domain Finset.univ shows that the 2 ^ n-bit slice of GapMCSP.yesSet s has formula size no larger than the (ofFunctionEncLength n (2 ^ n) (s n))-bit slice of SuccinctMCSP.enc '' SuccinctMCSP.

Stage 2: Finite-probability Adleman derandomization of a one-sided sample projection

theorem Cslib.Circuits.Boolean.two_pow_mul_pred_pow_lt {N k : ℕ} (hk : 1 ≤ k) : 2 ^ N * (k - 1) ^ (k * (N + 1)) < k ^ (k * (N + 1))

Elementary exponential inequality for Adleman amplification: for every k ≥ 1 and N : ℕ, 2 ^ N * (k - 1) ^ (k * (N + 1)) < k ^ (k * (N + 1)), corresponding to the real inequality 2 ^ N * (1 - 1 / k) ^ (k * (N + 1)) < 1.

theorem Cslib.Circuits.Boolean.exists_seed_tuple_of_one_sided_error {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {N k : ℕ} (hk : 1 ≤ k) (no : Finset (BitString N)) (Good : BitString N → Ω → Prop) [(T : BitString N) → (ω : Ω) → Decidable (Good T ω)] (hgood : ∀ T ∈ no, Fintype.card Ω ≤ k * (Finset.filter (Good T) Finset.univ).card) : ∃ (ωs : Fin (k * (N + 1)) → Ω), ∀ T ∈ no, ∃ (j : Fin (k * (N + 1))), Good T (ωs j)

Finite-probability Adleman amplification lemma. If no ⊆ BitString N is a set of negative inputs and, for every T ∈ no, at least a 1 / k-fraction of the seeds ω : Ω satisfy Good T ω (Fintype.card Ω ≤ k * (Finset.univ.filter (Good T)).card), then there exists a tuple ωs : Fin (k * (N + 1)) → Ω of k * (N + 1) seeds such that every T ∈ no is witnessed by at least one ωs j. Derived from Cslib.exists_cover_of_scaled_card_lt.

theorem Cslib.Circuits.Boolean.exists_seed_tuple_of_one_sided_error_real {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {N : ℕ} {δ : ℝ} (hδ : 0 < δ) (no : Finset (BitString N)) (Good : BitString N → Ω → Prop) [(T : BitString N) → (ω : Ω) → Decidable (Good T ω)] (hgood : ∀ T ∈ no, δ * ↑(Fintype.card Ω) ≤ ↑(Finset.filter (Good T) Finset.univ).card) : ∃ (ωs : Fin (⌈1 / δ⌉₊ * (N + 1)) → Ω), ∀ T ∈ no, ∃ (j : Fin (⌈1 / δ⌉₊ * (N + 1))), Good T (ωs j)

Real-parameter Adleman amplification lemma. If 0 < δ and every T ∈ no satisfies δ * Fintype.card Ω ≤ (Finset.univ.filter (Good T)).card, then ⌈1 / δ⌉₊ * (N + 1) seeds suffice to witness every T ∈ no.

theorem Cslib.Circuits.Boolean.exists_formula_separating_gapMCSP_of_succinctMCSP {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {s₁ s₂ : ℕ → ℕ} {n s k L : ℕ} (hk : 1 ≤ k) (hs : s₁ n ≤ s) (S : Ω → Finset (BitString n)) (hno : ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.noSet s₂ → Fintype.card Ω ≤ k * {ω : Ω | SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) (S ω) s ∉ SuccinctMCSP}.card) (hL : ∀ (ω : Ω), formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (SuccinctMCSP.ofFunctionEncLength n (S ω).card s)) ≤ L) : ∃ (F : Formula signature (2 ^ n)), F.leafSize ≤ k * (2 ^ n + 1) * L ∧ (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) ∧ ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.noSet s₂ → F.eval interpretation T = false

Stage 2 derandomization of an assumed one-sided sample projection (integer parameter k) ([OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]). Suppose s₁ n ≤ s, S : Ω → Finset (BitString n) is a family of sample sets indexed by a finite nonempty seed space Ω such that for every T : BitString (2 ^ n) with List.ofFn T ∈ GapMCSP.noSet s₂, at least a 1 / k-fraction of the seeds ω : Ω yield a no-instance SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) (S ω) s ∉ SuccinctMCSP, and each queried slice of SuccinctMCSP has formula size at most L. Then GapMCSP[s₁, s₂] on 2 ^ n-bit inputs is separated by a De Morgan formula of leaf size at most k * (2 ^ n + 1) * L.

theorem Cslib.Circuits.Boolean.exists_formula_separating_gapMCSP_of_succinctMCSP_real {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {s₁ s₂ : ℕ → ℕ} {n s L : ℕ} {δ : ℝ} (hδ : 0 < δ) (hs : s₁ n ≤ s) (S : Ω → Finset (BitString n)) (hno : ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.noSet s₂ → δ * ↑(Fintype.card Ω) ≤ ↑{ω : Ω | SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) (S ω) s ∉ SuccinctMCSP}.card) (hL : ∀ (ω : Ω), formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (SuccinctMCSP.ofFunctionEncLength n (S ω).card s)) ≤ L) : ∃ (F : Formula signature (2 ^ n)), F.leafSize ≤ ⌈1 / δ⌉₊ * (2 ^ n + 1) * L ∧ (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) ∧ ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.noSet s₂ → F.eval interpretation T = false

Stage 2 derandomization of an assumed one-sided sample projection (real error δ > 0) ([OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]). If S : Ω → Finset (BitString n) rejects each T ∈ GapMCSP.noSet s₂ with probability at least δ > 0 over a uniform seed ω ∈ Ω, and every queried slice of SuccinctMCSP has formula size at most L, then GapMCSP[s₁, s₂] on 2 ^ n-bit inputs is separated by a De Morgan formula of leaf size at most ⌈1 / δ⌉₊ * (2 ^ n + 1) * L.

theorem Cslib.Circuits.Boolean.exists_lt_formulaSize_succinctMCSP_of_gapMCSP {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {s₁ s₂ : ℕ → ℕ} {n s k L : ℕ} (hk : 1 ≤ k) (hs : s₁ n ≤ s) (S : Ω → Finset (BitString n)) (hno : ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.noSet s₂ → Fintype.card Ω ≤ k * {ω : Ω | SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) (S ω) s ∉ SuccinctMCSP}.card) (hged : ∀ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) → (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.noSet s₂ → F.eval interpretation T = false) → k * (2 ^ n + 1) * L < F.leafSize) : ∃ (ω : Ω), L < formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (SuccinctMCSP.ofFunctionEncLength n (S ω).card s))

Contrapositive Stage 2 derandomization for GapMCSP[s₁, s₂] ([OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]). If every De Morgan formula separating GapMCSP.yesSet s₁ and GapMCSP.noSet s₂ on 2 ^ n-bit inputs has leaf size strictly greater than k * (2 ^ n + 1) * L, then under an assumed one-sided sample projection S : Ω → Finset (BitString n) some seed ω : Ω produces a slice of SuccinctMCSP with formula size strictly greater than L.

theorem Cslib.Circuits.Boolean.exists_formula_separating_gapMCSP_of_partialMCSP {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {s₁ s₂ : ℕ → ℕ} {n s k L : ℕ} (hk : 1 ≤ k) (hs : s₁ n ≤ s) (S : Ω → Finset (BitString n)) (hno : ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.noSet s₂ → Fintype.card Ω ≤ k * {ω : Ω | PartialMCSP.Instance.restrictTable T (S ω) s ∉ PartialMCSP}.card) (hL : ∀ (ω : Ω), formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (SuccinctMCSP.ofFunctionEncLength n (S ω).card s)) ≤ L) : ∃ (F : Formula signature (2 ^ n)), F.leafSize ≤ k * (2 ^ n + 1) * L ∧ (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) ∧ ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.noSet s₂ → F.eval interpretation T = false

Stage 2 derandomization of an assumed one-sided sample projection phrased via PartialMCSP ([OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]). If s₁ n ≤ s, S : Ω → Finset (BitString n) rejects every T : BitString (2 ^ n) with List.ofFn T ∈ GapMCSP.noSet s₂ in the sense that PartialMCSP.Instance.restrictTable T (S ω) s ∉ PartialMCSP on at least a 1 / k-fraction of ω : Ω, and every queried slice of SuccinctMCSP has formula size at most L, then GapMCSP[s₁, s₂] on 2 ^ n-bit inputs is separated by a De Morgan formula of leaf size at most k * (2 ^ n + 1) * L.

Approximate (1, 1 - 1 / k)-MCSP and Stage 1 random-sampling projection

def Cslib.ApproxMCSP.noSet (s k : ℕ → ℕ) : Language Bool

The no-instances of approximate (1, 1 - 1 / k)-MCSP[s] [OliveiraSanthanam2018, Appendix A, Definition 41, p. 34]: the truth tables of n-input Boolean functions f such that every function g of circuit complexity at most s n agrees with f on at most a (1 - 1 / k n)-fraction of inputs (k n * (Finset.univ.filter fun x => g x = f x).card ≤ (k n - 1) * 2 ^ n).

@[simp]

theorem Cslib.ApproxMCSP.ofFn_mem_noSet_iff {s k : ℕ → ℕ} {n : ℕ} {T : BitString (2 ^ n)} : List.ofFn T ∈ noSet s k ↔ ∀ g ∈ Circuits.Boolean.computableFunctions n (s n), k n * {x : BitString n | g x = (MCSP.truthTable n).symm T x}.card ≤ (k n - 1) * 2 ^ n

A 2 ^ n-bit truth table T belongs to ApproxMCSP.noSet s k if and only if every g ∈ computableFunctions n (s n) agrees with (MCSP.truthTable n).symm T on at most a (1 - 1 / k n)-fraction of inputs.

theorem Cslib.ApproxMCSP.ofFn_mem_gapMCSP_noSet_of_mem_noSet {s k : ℕ → ℕ} {n : ℕ} (hk : 1 ≤ k n) {T : BitString (2 ^ n)} (hT : List.ofFn T ∈ noSet s k) : List.ofFn T ∈ GapMCSP.noSet s

When 1 ≤ k n, every approximate (1, 1 - 1 / k)-MCSP[s] no-instance on 2 ^ n bits is also a worst-case GapMCSP.noSet s no-instance.

theorem Cslib.ApproxMCSP.noSet_le_gapMCSP_noSet {s k : ℕ → ℕ} (hk : ∀ (n : ℕ), 1 ≤ k n) : noSet s k ≤ GapMCSP.noSet s

When 1 ≤ k n for all n, ApproxMCSP.noSet s k is contained in GapMCSP.noSet s.

theorem Cslib.ApproxMCSP.disjoint_yesSet_noSet {s₁ s₂ k : ℕ → ℕ} (hs : ∀ (n : ℕ), s₁ n ≤ s₂ n) (hk : ∀ (n : ℕ), 1 ≤ k n) : Disjoint (GapMCSP.yesSet s₁) (noSet s₂ k)

When s₁ n ≤ s₂ n and 1 ≤ k n for all n, no truth table is both a GapMCSP.yesSet s₁ yes-instance and an ApproxMCSP.noSet s₂ k no-instance.

def Cslib.ApproxMCSP (s₁ s₂ k : ℕ → ℕ) (hs : ∀ (n : ℕ), s₁ n ≤ s₂ n) (hk : ∀ (n : ℕ), 1 ≤ k n) : Complexity.PromiseProblem (List Bool)

ApproxMCSP[s₁, s₂, k] ((1, 1 - 1 / k)-MCSP [OliveiraSanthanam2018, Appendix A, Definition 41, p. 34]): the approximate MCSP promise problem whose yes-instances are truth tables of n-input Boolean functions with circuit complexity at most s₁ n and whose no-instances are truth tables of functions that disagree with every function of circuit complexity at most s₂ n on at least a 1 / k n-fraction of inputs, when s₁ n ≤ s₂ n and 1 ≤ k n for all n.

@[simp]

theorem Cslib.ApproxMCSP.yes_eq {s₁ s₂ k : ℕ → ℕ} (hs : ∀ (n : ℕ), s₁ n ≤ s₂ n) (hk : ∀ (n : ℕ), 1 ≤ k n) : (ApproxMCSP s₁ s₂ k hs hk).yes = GapMCSP.yesSet s₁

@[simp]

theorem Cslib.ApproxMCSP.no_eq {s₁ s₂ k : ℕ → ℕ} (hs : ∀ (n : ℕ), s₁ n ≤ s₂ n) (hk : ∀ (n : ℕ), 1 ≤ k n) : (ApproxMCSP s₁ s₂ k hs hk).no = noSet s₂ k

def Cslib.Circuits.Boolean.computableFunctionsLogBound (n s : ℕ) : ℕ

An explicit s log(n + s) upper bound on log₂ (computableFunctions n s).card, derived from card_computableFunctions_mul_factorial_le.

theorem Cslib.Circuits.Boolean.card_computableFunctions_le_two_pow (n s : ℕ) : (computableFunctions n s).card ≤ 2 ^ computableFunctionsLogBound n s

The number of n-input Boolean functions of De Morgan circuit complexity at most s is at most 2 ^ computableFunctionsLogBound n s.

theorem Cslib.Circuits.Boolean.card_le_two_mul_filter_notMem_succinctMCSP {n s k M : ℕ} (hk : 1 ≤ k) (hcard : (computableFunctions n s).card ≤ 2 ^ M) {f : BooleanFunction n} (hf : ∀ g ∈ computableFunctions n s, k * {x : BitString n | g x = f x}.card ≤ (k - 1) * 2 ^ n) : Fintype.card (Fin (k * (M + 2)) → BitString n) ≤ 2 * {ω : Fin (k * (M + 2)) → BitString n | SuccinctMCSP.Instance.ofFunction f (Finset.image ω Finset.univ) s ∉ SuccinctMCSP}.card

Oliveira–Santhanam Stage 1: random-sampling union bound over computableFunctions n s [OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]. Suppose 1 ≤ k, (computableFunctions n s).card ≤ 2 ^ M, and q = k * (M + 2). If every function g ∈ computableFunctions n s agrees with f : BooleanFunction n on at most a (1 - 1 / k)-fraction of inputs (k * (Finset.univ.filter fun x => g x = f x).card ≤ (k - 1) * 2 ^ n), then at least half of all q-tuples ω : Fin q → BitString n yield a no-instance SuccinctMCSP.Instance.ofFunction f (Finset.univ.image ω) s ∉ SuccinctMCSP.

theorem Cslib.Circuits.Boolean.exists_formula_separating_approxMCSP_of_succinctMCSP {s₁ s₂ k : ℕ → ℕ} {n M L : ℕ} (hk : 1 ≤ k n) (hs : s₁ n ≤ s₂ n) (hcard : (computableFunctions n (s₂ n)).card ≤ 2 ^ M) (hL : ∀ m ≤ k n * (M + 2), formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (SuccinctMCSP.ofFunctionEncLength n m (s₂ n))) ≤ L) : ∃ (F : Formula signature (2 ^ n)), F.leafSize ≤ (2 ^ n + 1) * L ∧ (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) ∧ ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ ApproxMCSP.noSet s₂ k → F.eval interpretation T = false

End-to-end Oliveira–Santhanam formula construction for approximate (1, 1 - 1 / k)-MCSP [OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]. Suppose 1 ≤ k n, s₁ n ≤ s₂ n, (computableFunctions n (s₂ n)).card ≤ 2 ^ M, and every (ofFunctionEncLength n m (s₂ n))-bit slice of SuccinctMCSP.enc '' SuccinctMCSP with m ≤ k n * (M + 2) has De Morgan formula size at most L. Then there exists a De Morgan formula F on 2 ^ n variables of leaf size at most (2 ^ n + 1) * L that separates GapMCSP.yesSet s₁ from ApproxMCSP.noSet s₂ k on 2 ^ n-bit truth tables.

theorem Cslib.Circuits.Boolean.exists_lt_formulaSize_succinctMCSP_of_approxMCSP {s₁ s₂ k : ℕ → ℕ} {n M L : ℕ} (hk : 1 ≤ k n) (hs : s₁ n ≤ s₂ n) (hcard : (computableFunctions n (s₂ n)).card ≤ 2 ^ M) (hged : ∀ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) → (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ ApproxMCSP.noSet s₂ k → F.eval interpretation T = false) → (2 ^ n + 1) * L < F.leafSize) : ∃ m ≤ k n * (M + 2), L < formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (SuccinctMCSP.ofFunctionEncLength n m (s₂ n)))

Contrapositive end-to-end formula hardness magnification for approximate (1, 1 - 1 / k)-MCSP [OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]. If 1 ≤ k n, s₁ n ≤ s₂ n, (computableFunctions n (s₂ n)).card ≤ 2 ^ M, and every De Morgan formula separating GapMCSP.yesSet s₁ and ApproxMCSP.noSet s₂ k on 2 ^ n-bit truth tables has leaf size strictly greater than (2 ^ n + 1) * L, then there exists m ≤ k n * (M + 2) such that the (ofFunctionEncLength n m (s₂ n))-bit slice of SuccinctMCSP.enc '' SuccinctMCSP has De Morgan formula size strictly greater than L.

theorem Cslib.Circuits.Boolean.exists_formula_separating_approxMCSP_of_succinctMCSP_inst {s₁ s₂ k : ℕ → ℕ} {n L : ℕ} (hs : ∀ (m : ℕ), s₁ m ≤ s₂ m) (hk : ∀ (m : ℕ), 1 ≤ k m) (hL : ∀ m ≤ k n * (computableFunctionsLogBound n (s₂ n) + 2), formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (SuccinctMCSP.ofFunctionEncLength n m (s₂ n))) ≤ L) : ∃ (F : Formula signature (2 ^ n)), F.leafSize ≤ (2 ^ n + 1) * L ∧ (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ (ApproxMCSP s₁ s₂ k hs hk).yes → F.eval interpretation T = true) ∧ ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ (ApproxMCSP s₁ s₂ k hs hk).no → F.eval interpretation T = false

Instantiated Oliveira–Santhanam formula construction for ApproxMCSP [OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14], with M instantiated to computableFunctionsLogBound n (s₂ n) via card_computableFunctions_le_two_pow. Every queried slice has encoded length SuccinctMCSP.ofFunctionEncLength n m (s₂ n) = 4 * n + 3 + m * (8 * n + 10) + s₂ n with m ≤ k n * (computableFunctionsLogBound n (s₂ n) + 2), i.e. O(k n ⋅ n ⋅ s₂ n ⋅ log(n + s₂ n)) bits, matching the slice length m(n) = Θ((n ⋅ s(n) ⋅ log s(n)) / δ(n)) of Lemma 16 for δ(n) = 1 / k n.

theorem Cslib.Circuits.Boolean.exists_lt_formulaSize_succinctMCSP_of_approxMCSP_inst {s₁ s₂ k : ℕ → ℕ} {n L : ℕ} (hs : ∀ (m : ℕ), s₁ m ≤ s₂ m) (hk : ∀ (m : ℕ), 1 ≤ k m) (hged : ∀ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ (ApproxMCSP s₁ s₂ k hs hk).yes → F.eval interpretation T = true) → (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ (ApproxMCSP s₁ s₂ k hs hk).no → F.eval interpretation T = false) → (2 ^ n + 1) * L < F.leafSize) : ∃ m ≤ k n * (computableFunctionsLogBound n (s₂ n) + 2), L < formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (SuccinctMCSP.ofFunctionEncLength n m (s₂ n)))

Instantiated contrapositive formula hardness magnification for ApproxMCSP [OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14], with M instantiated to computableFunctionsLogBound n (s₂ n) via card_computableFunctions_le_two_pow. The resulting hard slice of SuccinctMCSP.enc '' SuccinctMCSP has encoded length SuccinctMCSP.ofFunctionEncLength n m (s₂ n) = 4 * n + 3 + m * (8 * n + 10) + s₂ n with m ≤ k n * (computableFunctionsLogBound n (s₂ n) + 2), i.e. O(k n ⋅ n ⋅ s₂ n ⋅ log(n + s₂ n)) bits, matching m(n) = Θ((n ⋅ s(n) ⋅ log s(n)) / δ(n)) in Lemma 16 for δ(n) = 1 / k n.

Packaging Lemma 16 with SuccinctMCSP ∈ NP (Theorem 1 and Theorem 17)

def Cslib.Circuits.Boolean.approxMCSPQueryEncLength (n s k : ℕ) : ℕ

The maximum encoded bit length of a SuccinctMCSP.Instance.ofFunction query produced by the Stage 1 random-sampling projection at input length n, circuit-size threshold s, and error parameter k: SuccinctMCSP.ofFunctionEncLength n (k * (computableFunctionsLogBound n s + 2)) s.

theorem Cslib.Circuits.Boolean.ofFunctionEncLength_le_approxMCSPQueryEncLength {n m s k : ℕ} (hm : m ≤ k * (computableFunctionsLogBound n s + 2)) : SuccinctMCSP.ofFunctionEncLength n m s ≤ approxMCSPQueryEncLength n s k

Any query with m ≤ k * (computableFunctionsLogBound n s + 2) samples has encoded bit length at most approxMCSPQueryEncLength n s k.

theorem Cslib.Circuits.Boolean.exists_formula_separating_approxMCSP_of_agrees {L : Language Bool} (hag : ∀ (x : SuccinctMCSP.Instance), x ∈ SuccinctMCSP ↔ SuccinctMCSP.enc x ∈ L) {s₁ s₂ k : ℕ → ℕ} {n M B : ℕ} (hk : 1 ≤ k n) (hs : s₁ n ≤ s₂ n) (hcard : (computableFunctions n (s₂ n)).card ≤ 2 ^ M) (hB : ∀ m ≤ k n * (M + 2), formulaSize (L.slice (SuccinctMCSP.ofFunctionEncLength n m (s₂ n))) ≤ B) : ∃ (F : Formula signature (2 ^ n)), F.leafSize ≤ (2 ^ n + 1) * B ∧ (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) ∧ ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ ApproxMCSP.noSet s₂ k → F.eval interpretation T = false

End-to-end Oliveira–Santhanam formula construction for any language agreeing with SuccinctMCSP [OliveiraSanthanam2018, Section 3.1, Lemma 16, p. 14]. If L : Language Bool agrees with SuccinctMCSP along SuccinctMCSP.enc and every (ofFunctionEncLength n m (s₂ n))-bit slice of L with m ≤ k n * (M + 2) has De Morgan formula size at most B, then there exists a De Morgan formula F on 2 ^ n variables of leaf size at most (2 ^ n + 1) * B separating GapMCSP.yesSet s₁ from ApproxMCSP.noSet s₂ k on 2 ^ n-bit truth tables.

theorem Cslib.Circuits.Boolean.exists_formula_separating_approxMCSP_of_mem_FormulaSIZEOn {s₁ s₂ k r : ℕ → ℕ} (hs : ∀ (m : ℕ), s₁ m ≤ s₂ m) (hk : ∀ (m : ℕ), 1 ≤ k m) (hr : Monotone r) (hmem : SuccinctMCSP ∈ FormulaSIZEOn SuccinctMCSP.enc r) (n : ℕ) : ∃ (F : Formula signature (2 ^ n)), F.leafSize ≤ (2 ^ n + 1) * r (approxMCSPQueryEncLength n (s₂ n) (k n)) ∧ (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) ∧ ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ ApproxMCSP.noSet s₂ k → F.eval interpretation T = false

If SuccinctMCSP ∈ FormulaSIZEOn SuccinctMCSP.enc r for a monotone bound r, then ApproxMCSP has De Morgan formulas of leaf size (2 ^ n + 1) * r(m(n)) ([OliveiraSanthanam2018, Section 3.1, Lemma 16 and Theorem 17, pp. 14–15]).

theorem Cslib.Circuits.Boolean.not_succinctMCSP_mem_FormulaPolyOn_of_approxMCSP_hard {s₁ s₂ k : ℕ → ℕ} (hs : ∀ (m : ℕ), s₁ m ≤ s₂ m) (hk : ∀ (m : ℕ), 1 ≤ k m) (hhard : ∀ (c : ℕ), ∃ (n : ℕ), ∀ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) → (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ ApproxMCSP.noSet s₂ k → F.eval interpretation T = false) → (2 ^ n + 1) * (c * (approxMCSPQueryEncLength n (s₂ n) (k n) + 1) ^ c) < F.leafSize) : SuccinctMCSP ∉ FormulaPolyOn SuccinctMCSP.enc

Contrapositive of Oliveira–Santhanam Lemma 16 (general parameters, for SuccinctMCSP) [OliveiraSanthanam2018, Section 3.1, Lemma 16 and Theorem 17 (i)/(iii), pp. 14–15]. If s₁ n ≤ s₂ n and 1 ≤ k n for all n, and for every polynomial degree c : ℕ there exists an input length n at which every De Morgan formula separating GapMCSP.yesSet s₁ and ApproxMCSP.noSet s₂ k on 2 ^ n-bit truth tables has leaf size strictly greater than (2 ^ n + 1) * (c * (approxMCSPQueryEncLength n (s₂ n) (k n) + 1) ^ c), then SuccinctMCSP ∉ FormulaPolyOn SuccinctMCSP.enc.

theorem Cslib.Circuits.Boolean.not_NP_subset_FormulaPolyOn_of_approxMCSP_hard {s₁ s₂ k : ℕ → ℕ} (hs : ∀ (m : ℕ), s₁ m ≤ s₂ m) (hk : ∀ (m : ℕ), 1 ≤ k m) (hhard : ∀ (c : ℕ), ∃ (n : ℕ), ∀ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) → (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ ApproxMCSP.noSet s₂ k → F.eval interpretation T = false) → (2 ^ n + 1) * (c * (approxMCSPQueryEncLength n (s₂ n) (k n) + 1) ^ c) < F.leafSize) : ¬Complexity.NP SuccinctMCSP.enc ⊆ FormulaPolyOn SuccinctMCSP.enc

Contrapositive of Oliveira–Santhanam Lemma 16 (NP ⊄ Formula[poly], general parameters underlying Theorem 17(i)/(iii)) [OliveiraSanthanam2018, Section 3.1, Lemma 16 and Theorem 17 (i)/(iii), pp. 14–15]. Under the hypothesis of not_succinctMCSP_mem_FormulaPolyOn_of_approxMCSP_hard, combining Lemma 16 with SuccinctMCSP.mem_NP yields ¬ (Complexity.NP SuccinctMCSP.enc ⊆ FormulaPolyOn SuccinctMCSP.enc).

theorem Cslib.Circuits.Boolean.computableFunctionsLogBound_le_poly (n s : ℕ) : computableFunctionsLogBound n s ≤ (s + 1) * (2 * (n + s + 1) + 3)

Elementary polynomial upper bound on computableFunctionsLogBound n s: since Nat.clog 2 (n + s + 1) ≤ n + s + 1, we have computableFunctionsLogBound n s ≤ (s + 1) * (2 * (n + s + 1) + 3).

theorem Cslib.Circuits.Boolean.polynomiallyBounded_computableFunctionsLogBound {s : ℕ → ℕ} (hs : PolynomiallyBounded s) : PolynomiallyBounded fun (n : ℕ) => computableFunctionsLogBound n (s n)

When s is polynomially bounded, fun n => computableFunctionsLogBound n (s n) is polynomially bounded.

theorem Cslib.Circuits.Boolean.polynomiallyBounded_approxMCSPQueryEncLength {s k : ℕ → ℕ} (hs : PolynomiallyBounded s) (hk : PolynomiallyBounded k) : PolynomiallyBounded fun (n : ℕ) => approxMCSPQueryEncLength n (s n) (k n)

When the circuit-size threshold s and inverse-error parameter k are polynomially bounded in n, the maximum encoded query length fun n => approxMCSPQueryEncLength n (s n) (k n) is polynomially bounded in n.

theorem Cslib.Circuits.Boolean.exists_poly_formula_separating_approxMCSP_of_mem_FormulaPolyOn {s₁ s₂ k : ℕ → ℕ} (hs : ∀ (m : ℕ), s₁ m ≤ s₂ m) (hk : ∀ (m : ℕ), 1 ≤ k m) (hs₂_poly : PolynomiallyBounded s₂) (hk_poly : PolynomiallyBounded k) (hmem : SuccinctMCSP ∈ FormulaPolyOn SuccinctMCSP.enc) : ∃ (c : ℕ), ∀ (n : ℕ), ∃ (F : Formula signature (2 ^ n)), F.leafSize ≤ (2 ^ n + 1) * (c * (n + 1) ^ c) ∧ (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) ∧ ∀ (T : BitString (2 ^ n)), List.ofFn T ∈ ApproxMCSP.noSet s₂ k → F.eval interpretation T = false

Polynomial-parameter forward upper bound for Theorem 1(i) / Theorem 17(i) [OliveiraSanthanam2018, Section 1.2, Theorem 1 (i), p. 5; Section 3.1, Theorem 17 (i), p. 15]. If s₂ and k are polynomially bounded in n (for example s₂(n) = n ^ d and k(n) = (n + 1) ^ d) and SuccinctMCSP ∈ FormulaPolyOn SuccinctMCSP.enc, then there is a polynomial degree c : ℕ such that for every n, ApproxMCSP s₁ s₂ k on 2 ^ n-bit inputs is separated by a De Morgan formula of leaf size at most (2 ^ n + 1) * (c * (n + 1) ^ c) (N · (log N)^{O(1)} where N = 2 ^ n).

theorem Cslib.Circuits.Boolean.not_succinctMCSP_mem_FormulaPolyOn_of_approxMCSP_poly_hard {s₁ s₂ k : ℕ → ℕ} (hs : ∀ (m : ℕ), s₁ m ≤ s₂ m) (hk : ∀ (m : ℕ), 1 ≤ k m) (hs₂_poly : PolynomiallyBounded s₂) (hk_poly : PolynomiallyBounded k) (hhard : ∀ (c : ℕ), ∃ (n : ℕ), ∀ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) → (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ ApproxMCSP.noSet s₂ k → F.eval interpretation T = false) → (2 ^ n + 1) * (c * (n + 1) ^ c) < F.leafSize) : SuccinctMCSP ∉ FormulaPolyOn SuccinctMCSP.enc

Oliveira–Santhanam Theorem 1(i) / Theorem 17(i) (for SuccinctMCSP) [OliveiraSanthanam2018, Section 1.2, Theorem 1 (i), p. 5; Section 3.1, Theorem 17 (i), p. 15]. If s₂ and k are polynomially bounded in n (such as s(n) = n ^ d and δ(n) = n ^ (-d)), and ApproxMCSP[s₁, s₂, k] on N = 2 ^ n-bit truth tables is not separated by De Morgan formulas of leaf size (2 ^ n + 1) * (c * (n + 1) ^ c) (Formula[N · (log N)^{O(1)}]), then SuccinctMCSP ∉ FormulaPolyOn SuccinctMCSP.enc.

theorem Cslib.Circuits.Boolean.not_NP_subset_FormulaPolyOn_of_approxMCSP_poly_hard {s₁ s₂ k : ℕ → ℕ} (hs : ∀ (m : ℕ), s₁ m ≤ s₂ m) (hk : ∀ (m : ℕ), 1 ≤ k m) (hs₂_poly : PolynomiallyBounded s₂) (hk_poly : PolynomiallyBounded k) (hhard : ∀ (c : ℕ), ∃ (n : ℕ), ∀ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s₁ → F.eval interpretation T = true) → (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ ApproxMCSP.noSet s₂ k → F.eval interpretation T = false) → (2 ^ n + 1) * (c * (n + 1) ^ c) < F.leafSize) : ¬Complexity.NP SuccinctMCSP.enc ⊆ FormulaPolyOn SuccinctMCSP.enc

Oliveira–Santhanam Theorem 1(i) / Theorem 17(i) (Π[s, δ] ∉ Formula[N · (log N)^{O(1)}] ⟹ NP ⊄ Formula[poly]) [OliveiraSanthanam2018, Section 1.2, Theorem 1 (i), p. 5; Section 3.1, Theorem 17 (i), p. 15]. If s₂ and k are polynomially bounded in n and ApproxMCSP[s₁, s₂, k] on N = 2 ^ n-bit truth tables is not separated by De Morgan formulas of leaf size (2 ^ n + 1) * (c * (n + 1) ^ c), then ¬ (Complexity.NP SuccinctMCSP.enc ⊆ FormulaPolyOn SuccinctMCSP.enc).

Zero-Error Average-Case Formula Magnification (Lemma 26, Theorem 5, and Theorem 27)

theorem Cslib.Circuits.Boolean.card_filter_agreesOn_eq_two_pow (n : ℕ) (S : Finset (BitString n)) (g : BooleanFunction n) : {T : BitString (2 ^ n) | ∀ y ∈ S, (MCSP.truthTable n).symm T y = g y}.card = 2 ^ (2 ^ n - S.card)

For any fixed g : BooleanFunction n and sample set S : Finset (BitString n), the number of truth tables T : BitString (2 ^ n) whose function (MCSP.truthTable n).symm T agrees with g on every input in S is 2 ^ (2 ^ n - S.card) (since the S.card values on S are fixed to g and the remaining 2 ^ n - S.card values are unconstrained).

theorem Cslib.Circuits.Boolean.card_filter_ofFunction_mem_succinctMCSP_le (n : ℕ) (S : Finset (BitString n)) (s : ℕ) : {T : BitString (2 ^ n) | SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s ∈ SuccinctMCSP}.card ≤ (computableFunctions n s).card * 2 ^ (2 ^ n - S.card)

Oliveira–Santhanam Lemma 26 (finite-counting form) [OliveiraSanthanam2018, Section 3.3, Lemma 26, p. 21]: for any fixed subset S : Finset (BitString n) of distinct n-bit inputs and any circuit-size threshold s, the number of truth tables T : BitString (2 ^ n) whose restriction to S is consistent with a circuit of size at most s (SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s ∈ SuccinctMCSP) is at most (computableFunctions n s).card * 2 ^ (2 ^ n - S.card).

theorem Cslib.Circuits.Boolean.card_filter_ofFunction_mem_succinctMCSP_le_two_pow {n s M r : ℕ} {S : Finset (BitString n)} (hcard : (computableFunctions n s).card ≤ 2 ^ M) (hS : M + r ≤ S.card) : {T : BitString (2 ^ n) | SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s ∈ SuccinctMCSP}.card ≤ 2 ^ (2 ^ n - r)

Oliveira–Santhanam Lemma 26 (exponential-tail form) [OliveiraSanthanam2018, Section 3.3, Lemma 26, p. 21]: if (computableFunctions n s).card ≤ 2 ^ M (in particular for M = computableFunctionsLogBound n s) and M + r ≤ S.card, then at most 2 ^ (2 ^ n - r) truth tables T : BitString (2 ^ n) satisfy SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s ∈ SuccinctMCSP (so for r = n, at most a 2 ^ (-n)-fraction of all 2 ^ (2 ^ n) truth tables are consistent with a circuit of size at most s on S).

def Cslib.Circuits.Boolean.avgCaseMCSPQueryEncLength (n s r : ℕ) : ℕ

The encoded bit length of a SuccinctMCSP.Instance.ofFunction query on computableFunctionsLogBound n s + r distinct n-bit inputs at circuit-size threshold s, used in the zero-error average-case formula magnification of [OliveiraSanthanam2018, Section 3.3, Theorem 27, p. 21].

theorem Cslib.Circuits.Boolean.exists_formula_zero_error_average_case_of_sample {L : Language Bool} (hag : ∀ (x : SuccinctMCSP.Instance), x ∈ SuccinctMCSP ↔ SuccinctMCSP.enc x ∈ L) {s : ℕ → ℕ} {n r : ℕ} (S : Finset (BitString n)) (hS : computableFunctionsLogBound n (s n) + r ≤ S.card) : ∃ (F : Formula signature (2 ^ n)), F.leafSize ≤ formulaSize (L.slice (SuccinctMCSP.ofFunctionEncLength n S.card (s n))) ∧ (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s → F.eval interpretation T = true) ∧ {T : BitString (2 ^ n) | F.eval interpretation T = true}.card ≤ 2 ^ (2 ^ n - r)

Zero-error average-case formula projection for a given sample set S ([OliveiraSanthanam2018, Section 3.3, Lemma 26 and Theorem 27, p. 21]). If L : Language Bool agrees with SuccinctMCSP along SuccinctMCSP.enc and S : Finset (BitString n) satisfies computableFunctionsLogBound n (s n) + r ≤ S.card, then the single-query projection formula F on 2 ^ n variables has:

1. F.leafSize ≤ formulaSize (L.slice (SuccinctMCSP.ofFunctionEncLength n S.card (s n))) (no 2 ^ n blowup in formula size),
2. zero error on Yes-instances: ∀ T, List.ofFn T ∈ GapMCSP.yesSet s → F.eval interpretation T = true (so F.eval interpretation T = false certifies List.ofFn T ∉ GapMCSP.yesSet s), and
3. bounded acceptance on random truth tables: at most 2 ^ (2 ^ n - r) truth tables T : BitString (2 ^ n) satisfy F.eval interpretation T = true.

theorem Cslib.Circuits.Boolean.exists_formula_zero_error_average_case_of_agrees {L : Language Bool} (hag : ∀ (x : SuccinctMCSP.Instance), x ∈ SuccinctMCSP ↔ SuccinctMCSP.enc x ∈ L) {s : ℕ → ℕ} {n r : ℕ} (ht : computableFunctionsLogBound n (s n) + r ≤ 2 ^ n) : ∃ (F : Formula signature (2 ^ n)), F.leafSize ≤ formulaSize (L.slice (avgCaseMCSPQueryEncLength n (s n) r)) ∧ (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s → F.eval interpretation T = true) ∧ {T : BitString (2 ^ n) | F.eval interpretation T = true}.card ≤ 2 ^ (2 ^ n - r)

Zero-error average-case formula projection at exact query length avgCaseMCSPQueryEncLength [OliveiraSanthanam2018, Section 3.3, Theorem 27, p. 21]. Whenever computableFunctionsLogBound n (s n) + r ≤ 2 ^ n, choosing a subset S : Finset (BitString n) of cardinality computableFunctionsLogBound n (s n) + r yields a De Morgan formula F on 2 ^ n variables of leaf size at most formulaSize (L.slice (avgCaseMCSPQueryEncLength n (s n) r)) that accepts every T ∈ GapMCSP.yesSet s and accepts at most 2 ^ (2 ^ n - r) truth tables overall.

theorem Cslib.Circuits.Boolean.exists_formula_zero_error_average_case_of_succinctMCSP {s : ℕ → ℕ} {n r : ℕ} (ht : computableFunctionsLogBound n (s n) + r ≤ 2 ^ n) : ∃ (F : Formula signature (2 ^ n)), F.leafSize ≤ formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (avgCaseMCSPQueryEncLength n (s n) r)) ∧ (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s → F.eval interpretation T = true) ∧ {T : BitString (2 ^ n) | F.eval interpretation T = true}.card ≤ 2 ^ (2 ^ n - r)

Zero-error average-case formula projection for SuccinctMCSP.enc '' SuccinctMCSP [OliveiraSanthanam2018, Section 3.3, Theorem 27, p. 21].

theorem Cslib.Circuits.Boolean.lt_formulaSize_succinctMCSP_of_zero_error_average_case {s : ℕ → ℕ} {n r B : ℕ} (ht : computableFunctionsLogBound n (s n) + r ≤ 2 ^ n) (hhard : ∀ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s → F.eval interpretation T = true) → {T : BitString (2 ^ n) | F.eval interpretation T = true}.card ≤ 2 ^ (2 ^ n - r) → B < F.leafSize) : B < formulaSize (Language.slice (⇑SuccinctMCSP.enc '' SuccinctMCSP) (avgCaseMCSPQueryEncLength n (s n) r))

Contrapositive zero-error average-case formula magnification (Oliveira–Santhanam Theorem 27 at a single input length n) [OliveiraSanthanam2018, Section 3.3, Theorem 27, p. 21]. If computableFunctionsLogBound n (s n) + r ≤ 2 ^ n and every De Morgan formula F on 2 ^ n variables that accepts all GapMCSP.yesSet s truth tables and accepts at most 2 ^ (2 ^ n - r) truth tables overall has leaf size strictly greater than B, then the (avgCaseMCSPQueryEncLength n (s n) r)-bit slice of SuccinctMCSP.enc '' SuccinctMCSP has De Morgan formula size strictly greater than B.

theorem Cslib.Circuits.Boolean.not_succinctMCSP_mem_FormulaPolyOn_of_zero_error_average_case_hard {s r : ℕ → ℕ} (hhard : ∀ (c : ℕ), ∃ (n : ℕ), computableFunctionsLogBound n (s n) + r n ≤ 2 ^ n ∧ ∀ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s → F.eval interpretation T = true) → {T : BitString (2 ^ n) | F.eval interpretation T = true}.card ≤ 2 ^ (2 ^ n - r n) → c * (avgCaseMCSPQueryEncLength n (s n) (r n) + 1) ^ c < F.leafSize) : SuccinctMCSP ∉ FormulaPolyOn SuccinctMCSP.enc

One-sided zero-error average-case formula magnification (Oliveira–Santhanam Theorem 27, for SuccinctMCSP) [OliveiraSanthanam2018, Section 3.3, Theorem 27, p. 21; compare Section 1.2, Theorem 5, p. 8]. If for every polynomial degree c : ℕ there exists n : ℕ with computableFunctionsLogBound n (s n) + r n ≤ 2 ^ n such that every one-sided De Morgan formula for GapMCSP.yesSet s on 2 ^ n variables (accepting all GapMCSP.yesSet s instances and at most 2 ^ (2 ^ n - r n) truth tables overall) has leaf size strictly greater than c * (avgCaseMCSPQueryEncLength n (s n) (r n) + 1) ^ c, then SuccinctMCSP ∉ FormulaPolyOn SuccinctMCSP.enc.

theorem Cslib.Circuits.Boolean.not_NP_subset_FormulaPolyOn_of_zero_error_average_case_hard {s r : ℕ → ℕ} (hhard : ∀ (c : ℕ), ∃ (n : ℕ), computableFunctionsLogBound n (s n) + r n ≤ 2 ^ n ∧ ∀ (F : Formula signature (2 ^ n)), (∀ (T : BitString (2 ^ n)), List.ofFn T ∈ GapMCSP.yesSet s → F.eval interpretation T = true) → {T : BitString (2 ^ n) | F.eval interpretation T = true}.card ≤ 2 ^ (2 ^ n - r n) → c * (avgCaseMCSPQueryEncLength n (s n) (r n) + 1) ^ c < F.leafSize) : ¬Complexity.NP SuccinctMCSP.enc ⊆ FormulaPolyOn SuccinctMCSP.enc

One-sided zero-error average-case formula magnification (Oliveira–Santhanam Theorem 27, NP ⊄ Formula[poly]) [OliveiraSanthanam2018, Section 3.3, Theorem 27, p. 21; compare Section 1.2, Theorem 5, p. 8]. Under the hypothesis of not_succinctMCSP_mem_FormulaPolyOn_of_zero_error_average_case_hard, combining Theorem 27 with SuccinctMCSP.mem_NP yields ¬ (Complexity.NP SuccinctMCSP.enc ⊆ FormulaPolyOn SuccinctMCSP.enc).