Uniform indexed products of counting functions

A jointly uniform family on an encoded instance and a unary index admits products over a polynomial-time unary number of factors. Index-dependent certificates are padded to a common polynomially bounded row width, preserving their counts exactly. For GapP, expansion over Boolean choices reduces the product of differences to uniform #P products and a signed word sum.

Main definitions

• SharpP.indexedProductVerifier: check a separate indexed verifier on each certificate row.

Main results

• SharpP.acceptCount_indexedProductVerifier: exact cardinality factorization.
• SharpP.prod_range_mem: uniform indexed products preserve #P.
• GapP.prod_range_mem: uniform indexed products preserve GapP.

References

• S. Fenner, L. Fortnow, S. Kurtz, Gap-definable counting classes.

def Cslib.Complexity.SharpP.indexedProductVerifier {α : Type} (r k : α → ℕ) (V : (α × ℕ) × List Bool → Bool) (x : α × List Bool) : Bool

The verifier checks row i using the indexed instance (a, i), for every i < r(a).

theorem Cslib.Complexity.SharpP.polyTime_indexedProductVerifier {α : Type} {enc : α ↪ List Bool} {r k : α → ℕ} {V : (α × ℕ) × List Bool → Bool} (hr : Turing.MultiTapeTM.ComputableTidilyInPolyTime r enc Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableTidilyInPolyTime k enc Turing.MultiTapeTM.encUnary) (hV : Turing.MultiTapeTM.ComputableTidilyInPolyTime V (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (indexedProductVerifier r k V) (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

Uniform row counts, widths and indexed tests give a polynomial-time product verifier.

theorem Cslib.Complexity.SharpP.acceptCount_indexedProductVerifier {α : Type} (r k : α → ℕ) (V : (α × ℕ) × List Bool → Bool) (a : α) : acceptCount (indexedProductVerifier r k V) a (r a * k a) = ∏ i ∈ Finset.range (r a), acceptCount V (a, i) (k a)

Indexed row tuples have the product of their individual acceptance counts.

theorem Cslib.Complexity.SharpP.prod_range_mem {α : Type} {enc : α ↪ List Bool} {f : α × ℕ → ℕ} {r : α → ℕ} (hf : f ∈ SharpP (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encUnary)) (hr : Turing.MultiTapeTM.ComputableTidilyInPolyTime r enc Turing.MultiTapeTM.encUnary) : (fun (a : α) => ∏ i ∈ Finset.range (r a), f (a, i)) ∈ SharpP enc

A jointly uniform #P family on an instance and unary index may be multiplied over a polynomial-time unary range. If the original certificate polynomial is p, a common row width is p(2|a|+1+r(a)), and the unpadded total length is r(a) times that width.

theorem Cslib.Complexity.prod_sub_mul_eq_sum {n : ℕ} (f g : Fin n → ℤ) (c : ℤ) : ∏ i : Fin n, (f i - c * g i) = ∑ w : Fin n → Bool, (-c) ^ List.countP id (List.ofFn w) * ∏ i : Fin n, if w i = true then g i else f i

Expanding a product of (f i - c * g i) over Boolean choices pulls out (-c) to the number of true bits.

theorem Cslib.Complexity.GapP.prod_range_mem {α : Type} {enc : α ↪ List Bool} {g : α × ℕ → ℤ} {r : α → ℕ} (hg : g ∈ GapP (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encUnary)) (hr : Turing.MultiTapeTM.ComputableTidilyInPolyTime r enc Turing.MultiTapeTM.encUnary) : (fun (a : α) => ∏ i ∈ Finset.range (r a), g (a, i)) ∈ GapP enc

A jointly uniform GapP family on an instance and unary index may be multiplied over a polynomial-time unary range. Boolean expansion uses certified #P products and a polynomial-time parity sign, so no general GapP product closure is assumed.