refactor(ArthurMerlin): factor MA/AM amplification through BPP per-instance error bounds (#949)

Complexity/Computability/Circuit/Boolean/PolynomialTime.lean

@@ -179,6 +179,7 @@ theorem BPP_subset_PPolyOn : Complexity.BPP enc ⊆ PPolyOn enc := by
     (polynomiallyBounded_complexity_framedSlice hL' (by fun_prop)) (encodes enc)
     (encodesMember enc A) fun n x ⟨a, ha⟩ => by
       have h := hdec a
+      dsimp only [Complexity.BoundedErrorAt] at h
       rw [ha, List.length_ofFn] at h
       by_cases haA : a ∈ A
       · rw [(encodesMember_eq_true_iff ha).2 haA]

Complexity/Computability/Complexity/Classes/ArthurMerlin.lean

@@ -53,10 +53,13 @@ the second level of the polynomial hierarchy in
 ## Main definitions
 
 * `Cslib.Complexity.IsMerlinArthurVerifier`, `Cslib.Complexity.MA`.
+* `Cslib.Complexity.arthurMerlinSlice`: reply-existence counting slice of an Arthur–Merlin verifier.
 * `Cslib.Complexity.IsArthurMerlinVerifier`, `Cslib.Complexity.AM`.
 
 ## Main results
 
+* `Cslib.Complexity.isArthurMerlinVerifier_iff_decidesWithBoundedError`: an Arthur–Merlin verifier
+  is a bounded-error decider when composed with existential quantification over Merlin's reply.
 * `Cslib.Complexity.NP_subset_MA`, `Cslib.Complexity.BPP_subset_MA`.
 * `Cslib.Complexity.PolyTimeReducible.mem_MA`, `Cslib.Complexity.PolyTimeReducible.mem_AM`:
   closure under polynomial-time many-one reductions.
@@ -85,12 +88,10 @@ makes at least two thirds of the random strings `r` accepted, `V (a, y ++ r) = t
 non-member every proof leaves at least two thirds of the random strings rejected. -/
 def IsMerlinArthurVerifier (enc : α ↪ List Bool) (q p : Polynomial ℕ) (V : α × List Bool → Bool)
     (A : Set α) : Prop :=
-  ∀ a, (a ∈ A → ∃ y : Fin (q.eval (enc a).length) → Bool, 2 * 2 ^ p.eval (enc a).length ≤
-      3 * (univ.filter fun r : Fin (p.eval (enc a).length) → Bool =>
-        V (a, List.ofFn y ++ List.ofFn r) = true).card) ∧
-    (a ∉ A → ∀ y : Fin (q.eval (enc a).length) → Bool, 2 * 2 ^ p.eval (enc a).length ≤
-      3 * (univ.filter fun r : Fin (p.eval (enc a).length) → Bool =>
-        V (a, List.ofFn y ++ List.ofFn r) = false).card)
+  ∀ a, (a ∈ A → ∃ y : Fin (q.eval (enc a).length) → Bool,
+      BoundedErrorAt enc p (fun z => V (z.1, List.ofFn y ++ z.2)) a true) ∧
+    (a ∉ A → ∀ y : Fin (q.eval (enc a).length) → Bool,
+      BoundedErrorAt enc p (fun z => V (z.1, List.ofFn y ++ z.2)) a false)
 
 /-- The problems with polynomial-time Merlin–Arthur verifiers, with polynomially long proofs and
 random strings, with respect to the encoding `enc` of instances [Babai][Babai1985]. -/
@@ -105,6 +106,13 @@ theorem mem_MA : A ∈ MA enc ↔ ∃ (q p : Polynomial ℕ) (V : α × List Boo
 
 /-! ### Arthur–Merlin -/
 
+/-- Whether some reply `y` of length `q(|x.1|)` is accepted by `V` on `(x.1, x.2 ++ y)`.
+This is a counting device rather than a polynomial-time verifier: it quantifies over all
+`2 ^ q(|x.1|)` replies, and `DecidesWithBoundedError` carries no computability requirement. -/
+def arthurMerlinSlice (enc : α ↪ List Bool) (q : Polynomial ℕ) (V : α × List Bool → Bool)
+    (x : α × List Bool) : Bool :=
+  decide (∃ y : Fin (q.eval (enc x.1).length) → Bool, V (x.1, x.2 ++ List.ofFn y) = true)
+
 /-- `V` is an Arthur–Merlin verifier for `A`, with random strings of length `p` and replies of
 length `q`, both evaluated at the length of the encoded instance: on a member `a` at least two
 thirds of the random strings `r` have a reply `y` with `V (a, r ++ y) = true`; on a non-member at
@@ -118,6 +126,17 @@ def IsArthurMerlinVerifier (enc : α ↪ List Bool) (p q : Polynomial ℕ) (V :
       3 * (univ.filter fun r : Fin (p.eval (enc a).length) → Bool =>
         ∀ y : Fin (q.eval (enc a).length) → Bool, V (a, List.ofFn r ++ List.ofFn y) = false).card)
 
+/-- An Arthur–Merlin verifier is a bounded-error decider when composed with existential
+quantification over Merlin's reply. -/
+theorem isArthurMerlinVerifier_iff_decidesWithBoundedError {p q : Polynomial ℕ}
+    {V : α × List Bool → Bool} :
+    IsArthurMerlinVerifier enc p q V A ↔
+      DecidesWithBoundedError enc p (arthurMerlinSlice enc q V) A := by
+  simp only [IsArthurMerlinVerifier, DecidesWithBoundedError, PromiseProblem.SolvesWithBoundedError,
+    BoundedErrorAt, arthurMerlinSlice, decide_eq_true_iff, decide_eq_false_iff_not, not_exists,
+    Bool.not_eq_true]
+  rfl
+
 /-- The problems with polynomial-time Arthur–Merlin verifiers, with polynomially long random
 strings and replies, with respect to the encoding `enc` of instances
 [Babai][Babai1985], [Babai and Moran][BabaiMoran1988]. -/
@@ -147,9 +166,11 @@ theorem NP_subset_MA : NP enc ⊆ MA enc := by
   · obtain ⟨w, hw, hVw⟩ := (hA a).1 ha
     refine ⟨BitString.ofList _ w, two_mul_two_pow_le_card_filter_of_eq_zero
       (Polynomial.eval_zero) _ fun r => ?_⟩
+    dsimp only
     rw [BitString.ofFn_ofList hw,
       List.eq_nil_of_length_eq_zero (by simp : (List.ofFn r).length = 0), List.append_nil, hVw]
   · refine two_mul_two_pow_le_card_filter_of_eq_zero (Polynomial.eval_zero) _ fun r => ?_
+    dsimp only
     rw [List.eq_nil_of_length_eq_zero (by simp : (List.ofFn r).length = 0), List.append_nil]
     by_contra hVy
     exact ha ((hA a).2 ⟨_, List.length_ofFn, by simpa using hVy⟩)
@@ -218,6 +239,7 @@ theorem PolyTimeReducible.mem_MA {encB : β ↪ List Bool} {B : Set β}
   obtain ⟨q, p, V, hV, hVB⟩ := hB
   obtain ⟨Q, P, V', hV', hQe, hPe, hsplit⟩ := exists_truncated_verifier hf.tidy q p hV.tidy
   refine ⟨Q, P, V', .of_tidy hV', fun a => ?_⟩
+  dsimp only [BoundedErrorAt]
   simp only [hsplit]
   constructor
   · intro ha