Binomial coefficients of #P counts

If f is in #P and g is computed in polynomial time with unary output, then a ↦ C(f a, g a) is in #P Beigel and Gill, Property 8(ii) (Cslib.Complexity.SharpP.choose_mem). A certificate lists g a accepted certificates of the original verifier in strictly increasing lexicographic order, so each g a-element set of accepted certificates is counted exactly once.

The word test Cslib.Complexity.SharpP.subsetTest reads K rows of Z bits. The first k rows must be accepted by acc and strictly increasing, and the remaining rows must be zero, so it accepts C(N, k) words when acc accepts N words of length Z and k ≤ K (Cslib.Complexity.SharpP.card_filter_subsetTest). The extra zero rows let Toda's counting test use one row budget for every subset size (Cslib.Complexity.Toda.countingTest).

Main definitions

• Cslib.Complexity.SharpP.subsetTest: strictly increasing accepted rows, padded by zero rows.

Main results

• Cslib.Complexity.SharpP.card_filter_subsetTest: the test accepts C(N, k) words.
• Cslib.Complexity.SharpP.computableInPolyTime_subsetTest: the test runs in polynomial time.
• Cslib.Complexity.SharpP.choose_mem: binomial coefficients of #P counts are in #P.

References

• R. Beigel, J. Gill, Counting classes: thresholds, parity, mods, and fewness

def Cslib.Complexity.SharpP.subsetTest (acc : List Bool → Bool) (K Z k : ℕ) (zs : List Bool) : Bool

The k-subset test on K rows of Z bits: the first k rows are accepted by acc and strictly increasing, and the other rows are zero.

theorem Cslib.Complexity.SharpP.computableInPolyTime_subsetTest {γ : Type} {input : γ ↪ List Bool} {acc : γ → List Bool → Bool} (hacc : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : γ × List Bool) => acc p.1 p.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) {K Z k : γ → ℕ} {zs : γ → List Bool} (hK : Turing.MultiTapeTM.ComputableInPolyTime K input Turing.MultiTapeTM.encUnary) (hZ : Turing.MultiTapeTM.ComputableInPolyTime Z input Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableInPolyTime k input Turing.MultiTapeTM.encUnary) (hzs : Turing.MultiTapeTM.ComputableInPolyTime zs input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (c : γ) => subsetTest (acc c) (K c) (Z c) (k c) (zs c)) input Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.SharpP.card_filter_subsetTest (acc : List Bool → Bool) {K k : ℕ} (Z : ℕ) (hk : k ≤ K) : {zs : Fin (K * Z) → Bool | subsetTest acc K Z k (List.ofFn zs) = true}.card = {z : Fin Z → Bool | acc (List.ofFn z) = true}.card.choose k

The k-subset test counts k-element sets of accepted words, for k ≤ K.

theorem Cslib.Complexity.SharpP.choose_mem {α : Type} {enc : α ↪ List Bool} {f g : α → ℕ} (hf : f ∈ SharpP enc) (hg : Turing.MultiTapeTM.ComputableInPolyTime g enc Turing.MultiTapeTM.encUnary) : (fun (a : α) => (f a).choose (g a)) ∈ SharpP enc

Binomial coefficients of #P counts are in #P Beigel and Gill, Property 8(ii). If f is in #P with certificate length q(|a|) and g is computed in polynomial time in unary, the new certificate consists of g a rows of q(|a|) bits: accepted certificates of the original verifier in strictly increasing lexicographic order.