Polynomial-family robustness of WPP and LWPP

Uniform polynomial-time lists of nonzero binary integers may replace the single accepting target in WPP and LWPP. The accepting index is existential, with no computability assumption. For LWPP the list depends only on unary input length. List output size charges both the number of targets and their bit lengths; fixed finite lists are only a special case.

The interpolation product follows [Hemaspaandra et al., Theorems 3.1 and 3.7] [HHSW18]. We prove its uniform GapP membership by expanding over Boolean subsets: each term is a polynomial-time product of selected targets times a unary power of the gap. Thus the proof uses certified word sums and powers, without assuming indexed-product closure. The two-sided acceptance/rejection-target generalization is proved in WPP.TwoSided. Oracle lowness is a separate result.

The polynomial-time interfaces use Turing.MultiTapeTM.ComputableInPolyTime.

Main results

• GapP.prod_sub_mem: uniform interpolation products are GapP.
• mem_WPP_iff_exists_polyTime_targets, mem_LWPP_iff_exists_polyTime_targets: full one-sided polynomial-family robustness, stated with target lists.
• mem_WPP_of_polyTime_targets, mem_LWPP_of_polyTime_targets: list constructors.
• polyTime_indexedTargets: plain computability of an indexed target list.
• mem_WPP_of_indexed_targets, mem_LWPP_of_indexed_targets: indexed-family forms.

References

• [E. Hemaspaandra, L. A. Hemaspaandra, H. Spakowski, O. Watanabe, The Robustness of LWPP and WPP, with an Application to Graph Reconstruction] [HHSW18], Theorems 3.1 and 3.7.
• S. Fenner, L. Fortnow, S. Kurtz, Gap-definable counting classes.

theorem Cslib.Complexity.GapP.prod_sub_mem {α : Type} {enc : α ↪ List Bool} {f : α → List ℤ} {g : α → ℤ} (hf : Turing.MultiTapeTM.ComputableInPolyTime f enc (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hg : g ∈ GapP enc) : (fun (a : α) => (List.map (fun (z : ℤ) => z - g a) (f a)).prod) ∈ GapP enc

A product of differences between a uniformly computed list of binary FP targets and one GapP value is GapP. The list length and its total encoded size may depend polynomially on the input.

theorem Cslib.Complexity.mem_WPP_of_polyTime_targets {α : Type} {enc : α ↪ List Bool} {A : Set α} {g : α → ℤ} {f : α → List ℤ} (hg : g ∈ GapP enc) (hf : Turing.MultiTapeTM.ComputableInPolyTime f enc (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hn : ∀ (a : α), 0 ∉ f a) (hy : ∀ a ∈ A, g a ∈ f a) (hno : ∀ a ∉ A, g a = 0) : A ∈ WPP enc

Polynomial-family robustness of WPP. A GapP value which is zero on nonmembers and belongs to a uniformly computed list of nonzero binary integer targets on members witnesses WPP. The accepting target index need not be computable; the list length may vary with the input.

theorem Cslib.Complexity.mem_LWPP_of_polyTime_targets {α : Type} {enc : α ↪ List Bool} {A : Set α} {g : α → ℤ} {f : ℕ → List ℤ} (hg : g ∈ GapP enc) (hf : Turing.MultiTapeTM.ComputableInPolyTime f Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hn : ∀ (n : ℕ), 0 ∉ f n) (hy : ∀ a ∈ A, g a ∈ f (enc a).length) (hno : ∀ a ∉ A, g a = 0) : A ∈ LWPP enc

Polynomial-family robustness of LWPP. The target list is uniformly computed from unary input length. Its length may grow polynomially, and the accepting index is only existential.

def Cslib.Complexity.indexedTargets {α : Type} (f : α × ℕ → ℤ) (r : α → ℕ) (a : α) : List ℤ

The list of targets f (a, 0), ..., f (a, r a - 1) for an indexed target family.

theorem Cslib.Complexity.polyTime_indexedTargets {α : Type} {enc : α ↪ List Bool} {f : α × ℕ → ℤ} {r : α → ℕ} (hf : Turing.MultiTapeTM.ComputableInPolyTime f (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encIntBin) (hr : Turing.MultiTapeTM.ComputableInPolyTime r enc Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (indexedTargets f r) enc (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Uniformly indexed binary integer targets over a unary-computable range form a polynomial-time target list.

theorem Cslib.Complexity.mem_indexedTargets {α : Type} {f : α × ℕ → ℤ} {r : α → ℕ} {a : α} {z : ℤ} (h : ∃ i < r a, z = f (a, i)) : z ∈ indexedTargets f r a

A value matching f (a, i) for some i < r a belongs to indexedTargets f r a.

theorem Cslib.Complexity.mem_WPP_of_indexed_targets {α : Type} {enc : α ↪ List Bool} {A : Set α} {g : α → ℤ} {f : α × ℕ → ℤ} {r : α → ℕ} (hg : g ∈ GapP enc) (hf : Turing.MultiTapeTM.ComputableInPolyTime f (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encIntBin) (hr : Turing.MultiTapeTM.ComputableInPolyTime r enc Turing.MultiTapeTM.encUnary) (hn : ∀ (a : α), ∀ i < r a, f (a, i) ≠ 0) (hy : ∀ a ∈ A, ∃ i < r a, g a = f (a, i)) (hno : ∀ a ∉ A, g a = 0) : A ∈ WPP enc

Indexed polynomial-family WPP robustness, with a uniform binary-integer target function and a unary-computable number of targets. Indices run from zero to r a - 1; no procedure for selecting an accepting index is assumed. This includes [Hemaspaandra et al., Theorem 3.7] [HHSW18] by taking r a to be a polynomial in encoded input length.

theorem Cslib.Complexity.mem_LWPP_of_indexed_targets {α : Type} {enc : α ↪ List Bool} {A : Set α} {g : α → ℤ} {f : ℕ × ℕ → ℤ} {r : ℕ → ℕ} (hg : g ∈ GapP enc) (hf : Turing.MultiTapeTM.ComputableInPolyTime f (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encIntBin) (hr : Turing.MultiTapeTM.ComputableInPolyTime r Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hn : ∀ (n i : ℕ), i < r n → f (n, i) ≠ 0) (hy : ∀ a ∈ A, ∃ i < r (enc a).length, g a = f ((enc a).length, i)) (hno : ∀ a ∉ A, g a = 0) : A ∈ LWPP enc

Indexed polynomial-family LWPP robustness: both the target family and its size depend only on unary input length. Zero-based indexing translates the one-based family in Hemaspaandra et al., Theorem 3.1.

theorem Cslib.Complexity.mem_WPP_iff_exists_polyTime_targets {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ WPP enc ↔ ∃ g ∈ GapP enc, ∃ (f : α → List ℤ), Turing.MultiTapeTM.ComputableInPolyTime f enc (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) ∧ (∀ (a : α), 0 ∉ f a) ∧ (∀ a ∈ A, g a ∈ f a) ∧ ∀ a ∉ A, g a = 0

Poly-WPP = WPP, stated through uniformly computed lists of nonzero binary integer targets. A polynomial number of targets of polynomial bit length can be computed as one such list, and a singleton list gives the converse. This is the verifier-based form of Hemaspaandra et al., Theorem 3.7.

theorem Cslib.Complexity.mem_LWPP_iff_exists_polyTime_targets {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ LWPP enc ↔ ∃ g ∈ GapP enc, ∃ (f : ℕ → List ℤ), Turing.MultiTapeTM.ComputableInPolyTime f Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) ∧ (∀ (n : ℕ), 0 ∉ f n) ∧ (∀ a ∈ A, g a ∈ f (enc a).length) ∧ ∀ a ∉ A, g a = 0

Poly-LWPP = LWPP, with the target list computed from unary input length. This is the verifier-based form of Hemaspaandra et al., Theorem 3.1; the accepting index is not required to be computable.