refactor(mcsp): bundle GapMCSP as PromiseProblem and extract single-output and tableVerifier API

Complexity.lean

@@ -342,6 +342,7 @@ public import Complexity.Computability.Circuit.Clique
 public import Complexity.Computability.Circuit.Complexity
 public import Complexity.Computability.Circuit.CompositionDepth
 public import Complexity.Computability.Circuit.Continuity
+public import Complexity.Computability.Circuit.Counting
 public import Complexity.Computability.Circuit.Cyclic
 public import Complexity.Computability.Circuit.Cyclic.Feedback
 public import Complexity.Computability.Circuit.Decomposable

Complexity/Computability/Circuit/Complexity.lean

@@ -24,6 +24,8 @@ to each other.
 
 ## Main results
 
+* `Cslib.Circuits.Circuit.computesOn_single_iff`, `Cslib.Circuits.Circuit.computes_single_iff`:
+  a one-output circuit computes `single f` when its output `0` agrees with `f`.
 * `Cslib.Circuits.complexity_single_proj`, `Cslib.Circuits.one_le_complexity_single`: exactly the
   projections are computed without gates.
 * `Cslib.Circuits.complexity_single_unary_le`, `Cslib.Circuits.complexity_single_binary_le`:
@@ -47,6 +49,20 @@ variable {σ : Signature} {U : Type*} {I : Interpretation σ U} {n : ℕ}
 
 section Single
 
+/-- A one-output circuit computes `single f` on `S` exactly when its output `0` agrees with `f`
+on `S`. -/
+theorem Circuit.computesOn_single_iff {c : Circuit σ n 1} {S : Set (Fin n → U)}
+    {f : (Fin n → U) → U} :
+    c.ComputesOn I S (single f) ↔ ∀ x ∈ S, c.eval I x 0 = f x :=
+  ⟨fun h _ hx => congrFun (h hx) 0, fun h _ hx => funext fun i =>
+    Subsingleton.elim i 0 ▸ h _ hx⟩
+
+/-- A one-output circuit computes `single f` exactly when its output `0` agrees with `f` on
+every input. -/
+theorem Circuit.computes_single_iff {c : Circuit σ n 1} {f : (Fin n → U) → U} :
+    c.Computes I (single f) ↔ ∀ x, c.eval I x 0 = f x :=
+  ⟨fun h x => congrFun (h x) 0, fun h x => funext fun i => Subsingleton.elim i 0 ▸ h x⟩
+
 variable [I.IsComplete]
 
 /-- The coordinate projections cost no gates. -/
@@ -63,8 +79,8 @@ theorem one_le_complexity_single {f : (Fin n → U) → U} (hf : ∀ i, f ≠ fu
   cases hw : c.outputs 0 with
   | input i =>
     refine hf i (funext fun x => ?_)
-    have := congrFun (hc x) 0
-    simp only [Circuit.eval, Function.comp_apply, hw, Program.trace_input, single_apply] at this
+    have := Circuit.computes_single_iff.mp hc x
+    simp only [Circuit.eval, Function.comp_apply, hw, Program.trace_input] at this
     exact this.symm
   | gate j => exact absurd j.isLt (by omega)
 

Complexity/Computability/Circuit/Counting.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate (additions to `Cslib/Computability/Circuit/Counting.lean`)
+
+public import Complexity.Init
+public import Cslib.Computability.Circuit.Counting
+
+/-!
+# Counting functions computed by finite circuits over a complete basis
+
+This module provides the `complexity` characterization of `Cslib.Circuits.computableFunctions`
+over a complete gate basis, complementing
+`Cslib.Circuits.mem_computableFunctions_iff_ecomplexity_le`.
+
+## Main results
+
+* `Cslib.Circuits.mem_computableFunctions_iff_complexity_le`: over a complete basis, the scalar
+  functions computable with at most `s` gates are those of complexity at most `s`.
+-/
+
+@[expose] public section
+
+namespace Cslib.Circuits
+
+universe v u
+variable {σ : Signature.{v}} [Finite σ.Op] {U : Type u}
+variable {I : Interpretation σ U} [I.IsComplete] {n s : ℕ}
+
+/-- Over a complete basis, the functions computable with at most `s` gates are those of
+complexity at most `s`. -/
+theorem mem_computableFunctions_iff_complexity_le {f : (Fin n → U) → U} :
+    f ∈ computableFunctions I n s ↔ complexity I (single f) ≤ s := by
+  rw [mem_computableFunctions, complexity_le_iff]
+
+end Cslib.Circuits

Complexity/Computability/Complexity/Classes/PH/Kannan.lean

@@ -165,15 +165,11 @@ private theorem eventually_le_arity (k N : ℕ) : ∀ᶠ n in atTop, N ≤ arity
 
 /-! ### Hard truth tables -/
 
-/-- The function on `m` inputs with the truth table `T`, read as MCSP reads truth tables. -/
-def tableFunction (m : ℕ) (T : List Bool) : BooleanFunction m :=
-  fun y => MCSP.tableValue T (List.ofFn y)
-
 /-- `T` is a truth table on `arity k n` inputs whose function needs more than `threshold k n`
 gates. -/
 def IsHard (k n : ℕ) (T : List Bool) : Prop :=
   T.length = 2 ^ arity k n ∧
-    threshold k n < complexity interpretation (single (tableFunction (arity k n) T))
+    threshold k n < complexity interpretation (single (MCSP.tableFunction (arity k n) T))
 
 /-- `T` is the first hard truth table in lexicographic order: the hard table that is least as a
 binary number, most significant bit first. -/
@@ -200,20 +196,13 @@ theorem exists_isFirstHard {k n : ℕ} (h : ∃ T, IsHard k n T) : ∃ T, IsFirs
   obtain ⟨T, hT, hv⟩ := Nat.find_spec hex
   exact ⟨T, hT, fun T' hT' => hv ▸ Nat.find_min' hex ⟨T', hT', rfl⟩⟩
 
-/-- The truth table of a function, as a list, is read back as the function. -/
-private theorem tableFunction_ofFn_truthTable (m : ℕ) (f : BooleanFunction m) :
-    tableFunction m (List.ofFn (MCSP.truthTable m f)) = f := by
-  funext y
-  exact (MCSP.tableValue_ofFn ⟨m, MCSP.truthTable m f, 0⟩ y).trans
-    (by simp [MCSP.Instance.function])
-
 /-- **Shannon's counting argument**: hard truth tables exist at all large lengths. -/
 theorem eventually_exists_isHard (k : ℕ) : ∀ᶠ n in atTop, ∃ T, IsHard k n T := by
   obtain ⟨N, hN⟩ := Shannon.lt_complexity
   filter_upwards [eventually_le_arity k (max N 1), eventually_ge_atTop (k + 2)] with n hm hn
   obtain ⟨f, hf⟩ := hN (arity k n) (le_of_max_le_left hm)
   refine ⟨List.ofFn (MCSP.truthTable _ f), by simp, ?_⟩
-  rw [tableFunction_ofFn_truthTable]
+  rw [MCSP.tableFunction_ofFn_truthTable]
   have hm0 : (0 : ℝ) < arity k n := by exact_mod_cast (le_of_max_le_right hm)
   have hlt : (threshold k n : ℝ) * arity k n < 2 ^ arity k n := by
     exact_mod_cast threshold_mul_arity_lt (by omega)
@@ -269,44 +258,6 @@ theorem language_notMem_SIZE (k c : ℕ) : language k ∉ SIZE fun n => c * (n +
   have hpos : 1 ≤ (n + 1) ^ k := Nat.one_le_pow _ _ (by omega)
   nlinarith
 
-/-! ### Truth tables in MCSP -/
-
-/-- The MCSP instance of a truth table of length `2 ^ m`. -/
-private def tableInstance (m s : ℕ) (T : List Bool) (hT : T.length = 2 ^ m) : MCSP.Instance :=
-  ⟨m, fun i => T[i.val]'(by rw [hT]; exact i.isLt), s⟩
-
-private theorem ofFn_tableInstance {m s : ℕ} {T : List Bool} (hT : T.length = 2 ^ m) :
-    List.ofFn (tableInstance m s T hT).table = T := by
-  change List.ofFn (fun i : Fin (2 ^ m) => T[i.val]'(by rw [hT]; exact i.isLt)) = T
-  exact List.ext_getElem (by simp [hT]) fun _ _ _ => by simp
-
-private theorem function_tableInstance {m s : ℕ} {T : List Bool} (hT : T.length = 2 ^ m) :
-    (tableInstance m s T hT).function = tableFunction m T := by
-  funext y
-  rw [← MCSP.tableValue_ofFn, ofFn_tableInstance]
-  rfl
-
-/-- An accepted certificate for a truth table of length `2 ^ m` bounds the complexity of its
-function. -/
-private theorem complexity_le_of_tableVerifier {m s : ℕ} {T c : List Bool} (hT : T.length = 2 ^ m)
-    (h : MCSP.tableVerifier ((T, s), c) = true) :
-    complexity interpretation (single (tableFunction m T)) ≤ s := by
-  have := MCSP.mem_of_verifier_eq_true (x := tableInstance m s T hT) (w := c)
-    (by rw [MCSP.verifier_eq_tableVerifier, ofFn_tableInstance]; exact h)
-  rwa [MCSP.mem_iff, function_tableInstance] at this
-
-/-- A truth table of length `2 ^ m` whose function has at most `s` gates has a certificate of
-length `certLength m (MCSP.budget m s)`, accepted whatever bits follow it. -/
-private theorem exists_tableVerifier_append {m s : ℕ} {T : List Bool} (hT : T.length = 2 ^ m)
-    (h : complexity interpretation (single (tableFunction m T)) ≤ s) :
-    ∃ u : List Bool, u.length = certLength m (MCSP.budget m s) ∧
-      ∀ extra, MCSP.tableVerifier ((T, s), u ++ extra) = true := by
-  obtain ⟨u, hu, hV⟩ := MCSP.exists_verifier_append (x := tableInstance m s T hT)
-    (by rw [MCSP.mem_iff, function_tableInstance]; exact h)
-  refine ⟨u, hu, fun extra => ?_⟩
-  rw [← hV extra, MCSP.verifier_eq_tableVerifier, ofFn_tableInstance]
-  rfl
-
 /-! ### The `Σ₃` verifier -/
 
 /-- The length of the blocks holding truth tables. -/
@@ -411,10 +362,10 @@ private theorem isAlternatingVerifier_verifier (k : ℕ) :
         (BitString.binaryValue (table k x.length w₂) < BitString.binaryValue T →
           MCSP.tableVerifier ((table k x.length w₂, threshold k x.length), w₃) = true) := by
       by_cases hlt : BitString.binaryValue (table k x.length w₂) < BitString.binaryValue T
-      · have heasy : complexity interpretation (single (tableFunction (arity k x.length)
+      · have heasy : complexity interpretation (single (MCSP.tableFunction (arity k x.length)
             (table k x.length w₂))) ≤ threshold k x.length :=
           not_lt.1 fun h => absurd (hT.2 _ ⟨hT', h⟩) (not_le.2 hlt)
-        obtain ⟨u, hu, hV⟩ := exists_tableVerifier_append hT' heasy
+        obtain ⟨u, hu, hV⟩ := MCSP.exists_tableVerifier_append hT' heasy
         refine ⟨u ++ List.replicate (certBound k x.length - u.length) false, ?_, fun _ => hV _⟩
         have := certLength_le_certBound k x.length
         simp only [List.length_append, List.length_replicate]
@@ -428,7 +379,7 @@ private theorem isAlternatingVerifier_verifier (k : ℕ) :
     · cases hc : MCSP.tableVerifier ((T, threshold k x.length),
         w₂.drop (tableBound k x.length) ++ w₃)
       · rfl
-      · exact absurd (complexity_le_of_tableVerifier hT.1.1 hc) (not_le.2 hT.1.2)
+      · exact absurd (MCSP.complexity_le_of_tableVerifier hT.1.1 hc) (not_le.2 hT.1.2)
     · by_cases hlt : BitString.binaryValue (table k x.length w₂) < BitString.binaryValue T
       · exact Or.inr (hw₃ hlt)
       · exact Or.inl (not_lt.1 hlt)
@@ -458,7 +409,7 @@ private theorem isAlternatingVerifier_verifier (k : ℕ) :
     refine ⟨table k x.length w₁, ⟨⟨hT, ?_⟩, fun T' hT' => ?_⟩, ?_⟩
     · -- no circuit within the threshold computes the table
       by_contra hle
-      obtain ⟨u, hu, hV⟩ := exists_tableVerifier_append hT (not_lt.1 hle)
+      obtain ⟨u, hu, hV⟩ := MCSP.exists_tableVerifier_append hT (not_lt.1 hle)
       have hlen : (List.replicate (tableBound k x.length) false ++ u).length ≤
           tableBound k x.length + certBound k x.length := by
         have := certLength_le_certBound k x.length
@@ -474,7 +425,8 @@ private theorem isAlternatingVerifier_verifier (k : ℕ) :
         exact hM.trans (Nat.le_add_right _ _)
       obtain ⟨w₃, -, -, hw, -⟩ := key _ (hpad _ hlen)
       rw [table_append hT'.1] at hw
-      exact absurd (complexity_le_of_tableVerifier hT'.1 (hw (not_le.1 hlt))) (not_le.2 hT'.2)
+      exact absurd (MCSP.complexity_le_of_tableVerifier hT'.1 (hw (not_le.1 hlt)))
+        (not_le.2 hT'.2)
     · obtain ⟨w₃, -, -, -, hw⟩ := key _ (hpad [] (Nat.zero_le _))
       exact hw
 

Complexity/Computability/MCSP/AntiChecker.lean

@@ -9,7 +9,6 @@ module
 
 public import Complexity.Computability.MCSP.Succinct
 public import Complexity.Foundations.Data.BitString.Threshold
-import Complexity.Computability.Circuit.Complexity
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Data.Nat.Choose.Bounds
 
@@ -230,16 +229,17 @@ exactly when `f` needs more than `s` gates on `S`. -/
 theorem isAntiChecker_computableFunctions_iff {f : BooleanFunction n} {S : Set (BitString n)} :
     IsAntiChecker (computableFunctions n s) f S ↔ s < complexityOn interpretation S (single f) := by
   rw [← not_le, complexityOn_le_iff]
+  simp only [Circuit.computesOn_single_iff]
   constructor
   · rintro hS ⟨c, hc, hsize⟩
     obtain ⟨x, hx, hne⟩ := hS (fun y => c.eval interpretation y 0)
       (Boolean.mem_computableFunctions.mpr
-        ⟨c, fun y => funext fun i => by rw [Subsingleton.elim i 0]; rfl, hsize⟩)
-    exact hne (congrFun (hc hx) 0)
+        ⟨c, Circuit.computes_single_iff.mpr fun _ => rfl, hsize⟩)
+    exact hne (hc x hx)
   · intro h g hg
     obtain ⟨c, hcg, hsize⟩ := Boolean.mem_computableFunctions.mp hg
     by_contra! hgS
-    exact h ⟨c, fun x hx => funext fun i => (congrFun (hcg x) i).trans (hgS x hx), hsize⟩
+    exact h ⟨c, fun x hx => (Circuit.computes_single_iff.mp hcg x).trans (hgS x hx), hsize⟩
 
 /-- 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
@@ -276,7 +276,7 @@ theorem exists_lt_complexityOn {m b : ℕ} (hm : 0 < m) (hnm : n ≤ m) {f : Boo
     have hle := complexity_strictMajority_le g
     rw [heq] at hle
     have hsum : ∑ i, complexity interpretation (single (g i)) ≤ ∑ _i : Fin m, s :=
-      sum_le_sum fun i _ => mk_truthTable_mem_iff.mp (mk_truthTable_mem_iff_mem.mpr (hg i))
+      sum_le_sum fun i _ => mem_computableFunctions_iff_complexity_le.mp (hg i)
     simp only [sum_const, card_univ, Fintype.card_fin, smul_eq_mul] at hsum
     omega
   obtain ⟨S, hS, hanti⟩ := exists_isAntiChecker hm hα _ hmaj hb

Complexity/Computability/MCSP/Basic.lean

@@ -7,6 +7,9 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
+public import Complexity.Computability.Circuit.Complexity
+public import Complexity.Computability.Circuit.Counting
+public import Complexity.Computability.Complexity.Classes.Promise.Basic
 public import Complexity.Foundations.Data.BitString.Basic
 public import Cslib.Computability.Circuit.Boolean.Complexity
 public import Cslib.Computability.Circuit.Boolean.Counting
@@ -35,15 +38,17 @@ cslib's `computableFunctions n s`, so there are as many of them as such function
 
 * `Cslib.MCSP.truthTable`: truth tables of Boolean functions.
 * `Cslib.MCSP.Instance`, `Cslib.MCSP`: the instances and the yes-instances of MCSP.
-* `Cslib.GapMCSP.yes`, `Cslib.GapMCSP.no`: the two sides of `GapMCSP[s₁, s₂]`.
+* `Cslib.GapMCSP`: `GapMCSP[s₁, s₂]` as a `PromiseProblem`, with sides `Cslib.GapMCSP.yes` and
+  `Cslib.GapMCSP.no`.
 
 ## Main results
 
 * `Cslib.MCSP.mem_iff_exists_circuit`, `Cslib.MCSP.mem_iff_mem_computableFunctions`: the yes-
   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.disjoint_yes_no`: the promise of `GapMCSP[s₁, s₂]` is consistent when
-  `s₁ ≤ s₂`, and `Cslib.GapMCSP.no_eq_compl_yes`: `GapMCSP[s, s]` is MCSP at threshold `s`.
+  `s₁ ≤ s₂`, and `Cslib.GapMCSP.no_eq_compl_yes`, `Cslib.GapMCSP.eq_ofSet`: `GapMCSP[s, s]` is
+  MCSP at threshold `s`.
 
 ## References
 
@@ -120,8 +125,7 @@ most `s`. -/
 with at most `s` gates. -/
 theorem mk_truthTable_mem_iff_mem {f : BooleanFunction n} :
     ⟨n, truthTable n f, s⟩ ∈ MCSP ↔ f ∈ computableFunctions n s := by
-  rw [mk_truthTable_mem_iff, mem_computableFunctions_iff_ecomplexity_le, ← natCast_complexity]
-  exact Nat.cast_le.symm
+  rw [mk_truthTable_mem_iff, mem_computableFunctions_iff_complexity_le]
 
 /-- An instance is a yes-instance exactly when some circuit with at most `threshold` gates
 computes its function. -/
@@ -132,8 +136,8 @@ theorem mem_iff_exists_circuit {x : Instance} :
 
 /-- The yes-instances are the truth tables of the functions computable within the threshold. -/
 theorem mem_iff_mem_computableFunctions {x : Instance} :
-    x ∈ MCSP ↔ x.function ∈ computableFunctions x.arity x.threshold := by
-  rw [mem_iff_exists_circuit, mem_computableFunctions]
+    x ∈ MCSP ↔ x.function ∈ computableFunctions x.arity x.threshold :=
+  mem_computableFunctions_iff_complexity_le.symm
 
 /-- Raising the threshold keeps a yes-instance a yes-instance. -/
 theorem mem_of_le {T : BitString (2 ^ n)} (h : ⟨n, T, s⟩ ∈ MCSP) (hst : s ≤ t) :
@@ -148,7 +152,8 @@ theorem ncard_setOf_mem (n s : ℕ) :
       truthTable n '' (computableFunctions n s : Set (BooleanFunction n)) := by
     ext T
     obtain ⟨f, rfl⟩ := (truthTable n).surjective T
-    simp [complexity_le_iff]
+    simp only [Set.mem_ofPred_eq, mk_truthTable_mem_iff_mem, Set.mem_image, SetLike.mem_coe,
+      EmbeddingLike.apply_eq_iff_eq, exists_eq_right]
   rw [h, Set.ncard_image_of_injective _ (truthTable n).injective, Set.ncard_coe_finset]
 
 end MCSP
@@ -194,4 +199,30 @@ theorem no_anti {s₂' : ℕ → ℕ} (h : s₂ n ≤ s₂' n) : no s₂' n ⊆
 
 end GapMCSP
 
+/-- **`GapMCSP[s₁, s₂]` on functions of `n` inputs** [OliveiraPichSanthanam2019, Definition 2.4]:
+the promise problem whose yes-instances are the truth tables of functions with circuits of at most
+`s₁ n` gates and whose no-instances are those of functions that need more than `s₂ n` gates, when
+`s₁ n ≤ s₂ n`. -/
+def GapMCSP (s₁ s₂ : ℕ → ℕ) (n : ℕ) (h : s₁ n ≤ s₂ n) :
+    Complexity.PromiseProblem (BitString (2 ^ n)) where
+  yes := GapMCSP.yes s₁ n
+  no := GapMCSP.no s₂ n
+  disjoint := GapMCSP.disjoint_yes_no h
+
+namespace GapMCSP
+
+variable {s₁ s₂ : ℕ → ℕ} {n : ℕ}
+
+@[simp] theorem yes_eq (h : s₁ n ≤ s₂ n) : (GapMCSP s₁ s₂ n h).yes = yes s₁ n := rfl
+
+@[simp] theorem no_eq (h : s₁ n ≤ s₂ n) : (GapMCSP s₁ s₂ n h).no = no s₂ n := rfl
+
+/-- At equal thresholds `s`, `GapMCSP[s, s]` is the decision problem `GapMCSP.yes s n`, MCSP on
+`n` inputs at threshold `s`. -/
+@[simp] theorem eq_ofSet (s : ℕ → ℕ) (n : ℕ) :
+    GapMCSP s s n le_rfl = Complexity.PromiseProblem.ofSet (yes s n) :=
+  Complexity.PromiseProblem.ext rfl (no_eq_compl_yes s n)
+
+end GapMCSP
+
 end Cslib