Counting seeds by their prefix

The class verifier of the polynomial-time halting reduction reads only the first d bits of its seed of length d + e, so the number of seeds whose prefix satisfies a predicate is the number of prefixes that do, times 2 ^ e (length_filter_take). Together with length_filter_bitStrsOfLen this turns the verifier's seed count into the numerator of the compressed sampler's distribution CL.clDist.

theorem MIPRE.Cost.Data.bitStrsOfLen_succ (k : ℕ) : bitStrsOfLen (k + 1) = List.flatMap (fun (l : List Bool) => [false :: l, true :: l]) (bitStrsOfLen k)

theorem MIPRE.Cost.Data.length_filter_flatMap_bits (L : List BitStr) (p : BitStr → Bool) : (List.filter p (List.flatMap (fun (l : List Bool) => [false :: l, true :: l]) L)).length = (List.filter (fun (l : List Bool) => p (false :: l)) L).length + (List.filter (fun (l : List Bool) => p (true :: l)) L).length

Filtering the strings obtained by prepending a bit to each string of a list.

theorem MIPRE.Cost.Data.length_filter_take (Q : BitStr → Bool) (d e : ℕ) : (List.filter (fun (r : BitStr) => Q (List.take d r)) (bitStrsOfLen (d + e))).length = (List.filter Q (bitStrsOfLen d)).length * 2 ^ e

Counting by prefix: the strings of length d + e whose first d bits satisfy Q number the strings of length d satisfying Q, times 2 ^ e.