Counting the parities of a random string with one bit of a #P value

The second half of Toda's theorem Toda, Arora and Barak, Section 17.4: for numbers f r of accepted witnesses, given for the random strings r of length R, the number G of random strings with f r odd is read off one bit of a single counting function.

Modulus amplification by binomial coefficients

Toda's amplifier uses residues 0 modulo 2 ^ K for even counts and -1 for odd counts. This module uses the opposite sign: 0 for even counts and +1 for odd counts. Negating our amplifier modulo 2 ^ K recovers the 0/-1 convention. All subsequent counts and bit extraction here use the +1 convention, from the binomial expansion of (1 - 2) ^ c (Cslib.BitString.sum_range_neg_two_pow_mul_choose):

[c odd] = ∑ i < c, (-2) ^ i * choose c (i + 1),

whose terms with i ≥ K vanish modulo 2 ^ K (Cslib.BitString.sum_range_neg_two_pow_mul_choose_zmod). The coefficients (-2) ^ i are replaced by naturals equal to them modulo 2 ^ K (Cslib.Complexity.Toda.parityCoeff), and choose (f r) k counts the k-element sets of accepted witnesses, written as strictly increasing lists of k words for the lexicographic order (Cslib.BitString.card_filter_strictMono, Cslib.BitString.wordLt_ofFn_iff). So the words accepted by Cslib.Complexity.Toda.countingTest — a size k ≤ K in unary, one of parityCoeff K (k - 1) coefficient words, a random string r and a strictly increasing list of k accepted witnesses, padded with zero words — number H = ∑ i < K, parityCoeff K i * ∑ r, choose (f r) (i + 1) (Cslib.Complexity.Toda.card_filter_countingTest), and with K = R + 1, H is G modulo 2 ^ (R + 1) (Cslib.Complexity.Toda.cast_card_filter_countingTest).

One bit decides the majority

Cslib.Complexity.Toda.sharpTest accepts 2 H + 2 ^ R - 1 words (Cslib.Complexity.Toda.card_filter_sharpTest). Since G ≤ 2 ^ R, the bit R + 1 of this number says whether 2 G > 2 ^ R, that is whether more than half of the random strings have an odd number of accepted witnesses (Cslib.Complexity.Toda.testBit_card_filter_sharpTest).

Main definitions

• Cslib.Complexity.Toda.parityCoeff: the coefficients of the amplification.
• Cslib.Complexity.Toda.countingTest, Cslib.Complexity.Toda.sharpTest: the word tests of the counting functions.

Main results

• Cslib.Complexity.Toda.cast_card_filter_countingTest: the count is G modulo 2 ^ (R + 1).
• Cslib.Complexity.Toda.testBit_card_filter_sharpTest: one bit says whether 2 G > 2 ^ R.

References

• S. Toda, PP is as hard as the polynomial-time hierarchy
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

Modulus amplification

def Cslib.Complexity.Toda.parityCoeff (K i : ℕ) : ℕ

Natural coefficients equal to (-2) ^ i modulo 2 ^ K, for i ≤ K: 2 ^ i for even i and 2 ^ K - 2 ^ i for odd i.

Subsets as strictly increasing tuples

def Cslib.Complexity.Toda.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.Toda.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

The counting test

def Cslib.Complexity.Toda.unaryTest (K : ℕ) (kb : List Bool) : Bool

The unary test: kb is k bits true followed by falses, for its number k ≥ 1 of bits true.

theorem Cslib.Complexity.Toda.computableInPolyTime_unaryTest {γ : Type} {input : γ ↪ List Bool} {K : γ → ℕ} {kb : γ → List Bool} (hK : Turing.MultiTapeTM.ComputableInPolyTime K input Turing.MultiTapeTM.encUnary) (hkb : Turing.MultiTapeTM.ComputableInPolyTime kb input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (c : γ) => unaryTest (K c) (kb c)) input Turing.MultiTapeTM.encBool

def Cslib.Complexity.Toda.coeffTest (K k : ℕ) (cb : List Bool) : Bool

The coefficient test for size k: for odd k, the first K + 1 - k bits are false, and for even k, they are not all false.

theorem Cslib.Complexity.Toda.computableInPolyTime_coeffTest {γ : Type} {input : γ ↪ List Bool} {K k : γ → ℕ} {cb : γ → List Bool} (hK : Turing.MultiTapeTM.ComputableInPolyTime K input Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableInPolyTime k input Turing.MultiTapeTM.encUnary) (hcb : Turing.MultiTapeTM.ComputableInPolyTime cb input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (c : γ) => coeffTest (K c) (k c) (cb c)) input Turing.MultiTapeTM.encBool

def Cslib.Complexity.Toda.countingTest (accept : List Bool → List Bool → Bool) (K R Z : ℕ) (w : List Bool) : Bool

The counting test: a size k in unary in the first K bits, a coefficient word in the next K, a random string r in the next R, and a k-subset of words accepted by accept r in K rows of Z bits.

theorem Cslib.Complexity.Toda.card_filter_countingTest (accept : List Bool → List Bool → Bool) (K R Z : ℕ) : {w : Fin (K + (K + (R + K * Z))) → Bool | countingTest accept K R Z (List.ofFn w) = true}.card = ∑ i ∈ Finset.range K, parityCoeff K i * ∑ r : Fin R → Bool, {z : Fin Z → Bool | accept (List.ofFn r) (List.ofFn z) = true}.card.choose (i + 1)

The count of the counting test: ∑ i < K, parityCoeff K i * ∑ r, choose (f r) (i + 1), where f r counts the words accepted by accept r.

theorem Cslib.Complexity.Toda.cast_card_filter_countingTest (accept : List Bool → List Bool → Bool) (R Z : ℕ) : ↑{w : Fin (R + 1 + (R + 1 + (R + (R + 1) * Z))) → Bool | countingTest accept (R + 1) R Z (List.ofFn w) = true}.card = ↑{r : Fin R → Bool | Odd {z : Fin Z → Bool | accept (List.ofFn r) (List.ofFn z) = true}.card}.card

The count of the counting test is the number of random strings with an odd number of accepted words, modulo 2 ^ (R + 1), with sizes up to K = R + 1.

def Cslib.Complexity.Toda.sharpTest (accept : List Bool → List Bool → Bool) (R Z : ℕ) (w : List Bool) : Bool

The #P test: after a bit true, a free bit and the counting test; after a bit false, a word of R bits not all true, then falses.

theorem Cslib.Complexity.Toda.card_filter_sharpTest (accept : List Bool → List Bool → Bool) (R Z : ℕ) : {w : Fin (R + 1 + (R + 1 + (R + (R + 1) * Z)) + 1 + 1) → Bool | sharpTest accept R Z (List.ofFn w) = true}.card = 2 * {w : Fin (R + 1 + (R + 1 + (R + (R + 1) * Z))) → Bool | countingTest accept (R + 1) R Z (List.ofFn w) = true}.card + (2 ^ R - 1)

The #P test accepts 2 H + (2 ^ R - 1) words, for the count H of the counting test.

theorem Cslib.Complexity.Toda.testBit_card_filter_sharpTest (accept : List Bool → List Bool → Bool) (R Z : ℕ) : {w : Fin (R + 1 + (R + 1 + (R + (R + 1) * Z)) + 1 + 1) → Bool | sharpTest accept R Z (List.ofFn w) = true}.card.testBit (R + 1) = decide (2 ^ R < 2 * {r : Fin R → Bool | Odd {z : Fin Z → Bool | accept (List.ofFn r) (List.ofFn z) = true}.card}.card)

One bit of the #P count decides the majority: the bit R + 1 of the number of words accepted by the #P test says whether more than half of the random strings r of length R have an odd number of words accepted by accept r.

Polynomial time

theorem Cslib.Complexity.Toda.computableInPolyTime_countingTest {α : Type} {enc : α ↪ List Bool} {γ : Type} {input : γ ↪ List Bool} {V : (α × List Bool) × List Bool → Bool} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) {a : γ → α} {K R Z : γ → ℕ} {w : γ → List Bool} (ha : Turing.MultiTapeTM.ComputableInPolyTime a input enc) (hK : Turing.MultiTapeTM.ComputableInPolyTime K input Turing.MultiTapeTM.encUnary) (hR : Turing.MultiTapeTM.ComputableInPolyTime R input Turing.MultiTapeTM.encUnary) (hZ : Turing.MultiTapeTM.ComputableInPolyTime Z input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (c : γ) => countingTest (fun (r z : List Bool) => V ((a c, r), z)) (K c) (R c) (Z c) (w c)) input Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.Toda.computableInPolyTime_sharpTest {α : Type} {enc : α ↪ List Bool} {γ : Type} {input : γ ↪ List Bool} {V : (α × List Bool) × List Bool → Bool} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) {a : γ → α} {R Z : γ → ℕ} {w : γ → List Bool} (ha : Turing.MultiTapeTM.ComputableInPolyTime a input enc) (hR : Turing.MultiTapeTM.ComputableInPolyTime R input Turing.MultiTapeTM.encUnary) (hZ : Turing.MultiTapeTM.ComputableInPolyTime Z input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (c : γ) => sharpTest (fun (r z : List Bool) => V ((a c, r), z)) (R c) (Z c) (w c)) input Turing.MultiTapeTM.encBool

Toda's counting verifier has a plain polynomial-time certificate with the same captured input, two unary width parameters and word encoding as its machine-construction certificate.