feat(Computability/MCSP): MMW19 circuit magnification via Circuit-Min-Merge (#798)

Complexity.lean

@@ -866,6 +866,7 @@ public import Complexity.Computability.Kolmogorov.Uncomputability
 public import Complexity.Computability.Languages.Slice
 public import Complexity.Computability.MCSP.AntiChecker
 public import Complexity.Computability.MCSP.Basic
+public import Complexity.Computability.MCSP.Magnification
 public import Complexity.Computability.MCSP.NP
 public import Complexity.Computability.MCSP.Partial
 public import Complexity.Computability.MCSP.PartialETH

Complexity/Computability/Circuit/Boolean/PPoly.lean

@@ -44,8 +44,9 @@ language in `PPoly`.
   polynomial budget are in `P/poly`.
 * `Cslib.Circuits.Boolean.PPoly.compl`, `PPoly.sup`, `PPoly.inf`: closure under the Boolean
   operations.
-* `Cslib.Circuits.Boolean.mem_PPolyOn_encBits_iff`, `Cslib.Circuits.Boolean.PPolyOn.compl`:
-  agreement with `PPoly` on `encBits` and closure of `PPolyOn` under complement.
+* `Cslib.Circuits.Boolean.mem_PPolyOn_encBits_iff`, `Cslib.Circuits.Boolean.PPolyOn.compl`,
+  `Cslib.Circuits.Boolean.PPolyOn.sup`, `Cslib.Circuits.Boolean.PPolyOn.inf`: agreement with
+  `PPoly` on `encBits` and closure of `PPolyOn` under the Boolean operations.
 
 ## References
 
@@ -176,4 +177,18 @@ theorem compl_mem_PPolyOn_iff {α : Type*} {enc : α ↪ List Bool} {A : Set α}
     Aᶜ ∈ PPolyOn enc ↔ A ∈ PPolyOn enc :=
   ⟨fun h => by simpa using PPolyOn.compl h, PPolyOn.compl⟩
 
+/-- `PPolyOn` is closed under union. -/
+theorem PPolyOn.sup {α : Type*} {enc : α ↪ List Bool} {A B : Set α}
+    (hA : A ∈ PPolyOn enc) (hB : B ∈ PPolyOn enc) : (A ∪ B : Set α) ∈ PPolyOn enc := by
+  obtain ⟨LA, hLA, hA⟩ := hA
+  obtain ⟨LB, hLB, hB⟩ := hB
+  exact ⟨LA ⊔ LB, PPoly.sup hLA hLB, fun a => by rw [Set.mem_union, hA a, hB a]; rfl⟩
+
+/-- `PPolyOn` is closed under intersection. -/
+theorem PPolyOn.inf {α : Type*} {enc : α ↪ List Bool} {A B : Set α}
+    (hA : A ∈ PPolyOn enc) (hB : B ∈ PPolyOn enc) : (A ∩ B : Set α) ∈ PPolyOn enc := by
+  obtain ⟨LA, hLA, hA⟩ := hA
+  obtain ⟨LB, hLB, hB⟩ := hB
+  exact ⟨LA ⊓ LB, PPoly.inf hLA hLB, fun a => by rw [Set.mem_inter_iff, hA a, hB a]; rfl⟩
+
 end Cslib.Circuits.Boolean

Complexity/Computability/Complexity/Classes/PH/KarpLipton.lean

@@ -72,8 +72,10 @@ equivalent to `SAT ∈ PPolyOn encCNF` (`Cslib.Complexity.NP_subset_PPolyOn_iff_
 * `Cslib.Complexity.PH_eq_SigmaP_two_of_NP_subset_PPoly`: if `NP ⊆ P/poly`, then `PH = Σ₂`.
 * `Cslib.Complexity.PolyTimeReducible.mem_PPolyOn`: preimages of `P/poly` are closed under
   polynomial-time many-one reductions.
-* `Cslib.Complexity.mem_PPoly_of_exists_frame_append`: nonuniform existential quantifier
-  elimination in `P/poly` under `NP ⊆ P/poly`.
+* `Cslib.Complexity.mem_PPoly_of_exists_frame_append`,
+  `Cslib.Complexity.PPolyOn.exists_of_computableInPolyTime_length`,
+  `Cslib.Complexity.PPolyOn.forall_of_computableInPolyTime_length`: nonuniform existential and
+  universal quantifier elimination in `P/poly` under `NP ⊆ P/poly`.
 * `Cslib.Complexity.SigmaP_subset_PPolyOn_of_NP_subset_PPoly`,
   `Cslib.Complexity.PiP_subset_PPolyOn_of_NP_subset_PPoly`,
   `Cslib.Complexity.PH_subset_PPolyOn_of_NP_subset_PPoly`: if `NP ⊆ P/poly`, then `Σₖ ⊆ P/poly`,
@@ -308,6 +310,62 @@ theorem mem_PPoly_of_exists_frame_append
       rw [List.length_take, hw, Nat.min_eq_left hle]
     exact ⟨w.take (p.eval x.length), htake, (hV_frame _ htake).1 hwV⟩
 
+/-- **Nonuniform existential quantifier elimination in `PPolyOn`.** Under `NP ⊆ P/poly`, if a
+relation `P : α → List Bool → Prop` is in `PPolyOn (encPair enc encBits)` and the witness length
+`N : α → ℕ` is computable in polynomial time in unary, then `{a | ∃ u, u.length = N a ∧ P a u}` is
+in `PPolyOn enc`. -/
+theorem PPolyOn.exists_of_computableInPolyTime_length
+    (hNP : NP encBits ⊆ PPolyOn encBits) {N : α → ℕ}
+    (hN : ComputableInPolyTime N enc encUnary) {P : α → List Bool → Prop}
+    (hP : {p : α × List Bool | P p.1 p.2} ∈ PPolyOn (encPair enc encBits)) :
+    {a : α | ∃ u : List Bool, u.length = N a ∧ P a u} ∈ PPolyOn enc := by
+  let B : Set (α × List Bool) := {p | P p.1 (p.2.take (N p.1))}
+  have hred : PolyTimeReducible (encPair enc encBits) (encPair enc encBits)
+      B {p : α × List Bool | P p.1 p.2} := by
+    refine ⟨fun p => (p.1, p.2.take (N p.1)), ?_, fun _ => Iff.rfl⟩
+    exact .of_tidy ((ComputableTidilyInPolyTime.fst enc encBits).prod
+      (ComputableTidilyInPolyTime.bitsTakeWithInput
+        (ComputableTidilyInPolyTime.snd enc encBits)
+        (hN.tidy.comp (ComputableTidilyInPolyTime.fst enc encBits))))
+  obtain ⟨M, hM, hBM⟩ := hred.mem_PPolyOn hP
+  obtain ⟨p, hp⟩ := hN.tidy.polyBounded.exists_polynomial
+  refine ⟨{x : List Bool | ∃ w : List Bool, w.length = p.eval x.length ∧ frame x ++ w ∈ M},
+    mem_PPoly_of_exists_frame_append hNP hM p, fun a => ?_⟩
+  have hle : N a ≤ p.eval (enc a).length := hp a
+  constructor
+  · rintro ⟨u, hu, hPu⟩
+    refine ⟨u ++ List.replicate (p.eval (enc a).length - N a) false,
+      by rw [List.length_append, List.length_replicate, hu, Nat.add_sub_cancel' hle], ?_⟩
+    have htake : (u ++ List.replicate (p.eval (enc a).length - N a) false).take (N a) = u := by
+      rw [← hu, List.take_left]
+    have hmem : (a, u ++ List.replicate (p.eval (enc a).length - N a) false) ∈ B := by
+      change P a ((u ++ List.replicate (p.eval (enc a).length - N a) false).take (N a))
+      rwa [htake]
+    simpa [encPair_apply, encBits_apply] using (hBM _).1 hmem
+  · rintro ⟨w, hw, hwM⟩
+    have hmem : (a, w) ∈ B :=
+      (hBM (a, w)).2 (by simpa [encPair_apply, encBits_apply] using hwM)
+    refine ⟨w.take (N a), ?_, hmem⟩
+    rw [List.length_take, hw, Nat.min_eq_left hle]
+
+/-- **Nonuniform universal quantifier elimination in `PPolyOn`.** Under `NP ⊆ P/poly`, if a
+relation `P : α → List Bool → Prop` is in `PPolyOn (encPair enc encBits)` and the bound `N : α → ℕ`
+is computable in polynomial time in unary, then `{a | ∀ u, u.length = N a → P a u}` is in
+`PPolyOn enc`. -/
+theorem PPolyOn.forall_of_computableInPolyTime_length
+    (hNP : NP encBits ⊆ PPolyOn encBits) {N : α → ℕ}
+    (hN : ComputableInPolyTime N enc encUnary) {P : α → List Bool → Prop}
+    (hP : {p : α × List Bool | P p.1 p.2} ∈ PPolyOn (encPair enc encBits)) :
+    {a : α | ∀ u : List Bool, u.length = N a → P a u} ∈ PPolyOn enc := by
+  have hex : {a : α | ∃ u : List Bool, u.length = N a ∧ ¬ P a u} ∈ PPolyOn enc :=
+    PPolyOn.exists_of_computableInPolyTime_length hNP hN (PPolyOn.compl hP)
+  have h_eq : {a : α | ∀ u : List Bool, u.length = N a → P a u} =
+      {a : α | ∃ u : List Bool, u.length = N a ∧ ¬ P a u}ᶜ := by
+    ext a
+    simp
+  rw [h_eq]
+  exact PPolyOn.compl hex
+
 /-- **Karp–Lipton, `NP ⊆ P/poly ⇒ Σₖ ⊆ P/poly`.** If `NP ⊆ P/poly` over bitstrings, then every
 level `Σₖ` of the polynomial hierarchy, with any encoding of its instances, is in `P/poly`
 [Karp and Lipton, Section 3][KarpLipton1980], [Arora and Barak, Section 6.4][AroraBarak09]. -/
@@ -321,13 +379,14 @@ theorem SigmaP_subset_PPolyOn_of_NP_subset_PPoly
   | succ k ih =>
     intro A hA
     obtain ⟨p, B, hB, hAB⟩ := exists_mem_PiP_of_mem_SigmaP_succ hA
-    obtain ⟨M₀, hM₀, hBM₀⟩ := ih (compl_mem_SigmaP_of_mem_PiP hB)
-    have hM : M₀ᶜ ∈ PPoly := PPoly.compl hM₀
-    refine ⟨{x : List Bool | ∃ w : List Bool, w.length = p.eval x.length ∧ frame x ++ w ∈ M₀ᶜ},
-      mem_PPoly_of_exists_frame_append hNP hM p, fun a => (hAB a).trans ?_⟩
-    exact exists_congr fun w => and_congr_right fun _ => by
-      have := (hBM₀ (a, w)).not
-      rwa [Set.mem_compl_iff, Classical.not_not, encPair_apply, encBits_apply] at this
+    have hB_PPoly : B ∈ PPolyOn (encPair enc encBits) := by
+      simpa using PPolyOn.compl (ih (compl_mem_SigmaP_of_mem_PiP hB))
+    have hN : ComputableInPolyTime (fun a : α => p.eval (enc a).length) enc encUnary :=
+      (unary_eval p).comp (encoding_length enc)
+    have hA_eq : A = {a : α | ∃ w : List Bool, w.length = p.eval (enc a).length ∧ (a, w) ∈ B} :=
+      Set.ext hAB
+    rw [hA_eq]
+    exact PPolyOn.exists_of_computableInPolyTime_length hNP hN hB_PPoly
 
 /-- **Karp–Lipton, `NP ⊆ P/poly ⇒ Πₖ ⊆ P/poly`.** If `NP ⊆ P/poly` over bitstrings, then every
 level `Πₖ` of the polynomial hierarchy, with any encoding of its instances, is in `P/poly`. -/

Complexity/Computability/MCSP/Basic.lean

@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Circuit.Complexity
 public import Complexity.Computability.Circuit.Counting
 public import Complexity.Computability.Complexity.Classes.Promise.Basic
+public import Complexity.Computability.Languages.Slice
 public import Complexity.Foundations.Data.BitString.Basic
 public import Cslib.Computability.Circuit.Boolean.Complexity
 public import Cslib.Computability.Circuit.Boolean.Counting
@@ -51,6 +52,7 @@ cslib's `computableFunctions n s`, so there are as many of them as such function
   instances of MCSP, as circuits and as computable functions.
 * `Cslib.MCSP.ncard_setOf_mem`: the number of yes-instances of a given arity and threshold.
 * `Cslib.GapMCSP.ofFn_mem_yesSet_iff_mem_MCSP`,
+  `Cslib.GapMCSP.slice_yesSet_eq_true_iff`,
   `Cslib.GapMCSP.ofFn_mem_noSet_iff_notMem_MCSP`: characterization of truth tables of length `2^n`
   in the yes and no sets.
 * `Cslib.GapMCSP.disjoint_yesSet_noSet`: the promise of `GapMCSP[s₁, s₂]` is consistent when
@@ -218,6 +220,13 @@ theorem ofFn_mem_yesSet_iff_mem_MCSP {n : ℕ} {T : BitString (2 ^ n)} :
     List.ofFn T ∈ yesSet s₁ ↔ (⟨n, T, s₁ n⟩ : MCSP.Instance) ∈ MCSP :=
   ofFn_mem_yesSet_iff
 
+/-- The `2 ^ n`-bit slice of `yesSet s₁` evaluates to `true` on `T` if and only if its circuit
+complexity is at most `s₁ n`. -/
+theorem slice_yesSet_eq_true_iff {n : ℕ} {T : BitString (2 ^ n)} :
+    (yesSet s₁).slice (2 ^ n) T = true ↔
+      complexity interpretation (single ((truthTable n).symm T)) ≤ s₁ n := by
+  rw [Language.slice_eq_true_iff, ofFn_mem_yesSet_iff]
+
 /-- A `2 ^ n`-bit string `T`, viewed as a list via `List.ofFn`, belongs to `noSet s₂`
 if and only if its circuit complexity is strictly greater than `s₂ n`. -/
 @[simp] theorem ofFn_mem_noSet_iff {n : ℕ} {T : BitString (2 ^ n)} :