Acceptance counts and uniform probabilities

The count of accepted random words is exactly their probability under a uniform word source multiplied by the number of words. This connects counting-based verifier contracts to ordinary probability bounds without changing the verifier's behavior on malformed random strings.

Main results

• Cslib.Complexity.uniformList_acceptCount: the exact uniform acceptance probability.
• Cslib.Complexity.uniformList_acceptCount_toReal: the same identity over the reals.
• Cslib.Complexity.acceptCount_le_half_iff: equivalence of the integer and probability bounds.

theorem Cslib.Complexity.uniformList_acceptCount {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : (PMF.map (fun (word : List Bool) => V (a, word)) (BitString.uniformList n)) true = ↑(acceptCount V a n) / 2 ^ n

A counted verifier's uniform acceptance probability is its accepted fraction of all words.

theorem Cslib.Complexity.uniformList_acceptCount_toReal {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : ((PMF.map (fun (word : List Bool) => V (a, word)) (BitString.uniformList n)) true).toReal = ↑(acceptCount V a n) / 2 ^ n

The accepted fraction has the same ordinary real-valued interpretation.

theorem Cslib.Complexity.acceptCount_le_half_iff {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : 2 * acceptCount V a n ≤ 2 ^ n ↔ ((PMF.map (fun (word : List Bool) => V (a, word)) (BitString.uniformList n)) true).toReal ≤ 1 / 2

Accepting at most half the random words is equivalent to probability at most one half.