Reading a count off a digit

What a counting reduction with one oracle call needs of arithmetic: a sum of powers ∑ i, B ^ m i is a number in base B whose digit of rank p is the number of indices i with m i = p, as long as each of those numbers is below B (DescriptiveComplexity.sum_pow_div_mod). A gadget that multiplies the solutions of weight p by B ^ p therefore lets a quotient and a remainder count the solutions of one weight.

Also here: a finite set with k elements has 2 ^ k subsets, stated for predicates (DescriptiveComplexity.card_subsets_eq_two_pow).

theorem DescriptiveComplexity.card_subsets_eq_two_pow {α : Type} [Finite α] (p : α → Prop) : Nat.card { ν : α → Prop // ∀ (x : α), ν x → p x } = 2 ^ Nat.card { x : α // p x }

The sets of elements satisfying p are as many as two to the number of such elements.

theorem DescriptiveComplexity.sum_pow_div_mod {ι : Type} [Fintype ι] (m : ι → ℕ) {B : ℕ} (hB : 0 < B) (h : ∀ (q : ℕ), {i : ι | m i = q}.card < B) (p : ℕ) : (∑ i : ι, B ^ m i) / B ^ p % B = {i : ι | m i = p}.card

Digit extraction: in the sum ∑ i, B ^ m i, read in base B, the digit of rank p is the number of indices of exponent p, when fewer than B indices share each exponent.