Verifying formula counts over a supplied field

Each satisfying Boolean input contributes $1_F$ and each other input contributes $0_F$ by Boolean agreement. Adding the $2^n$ values gives $M{1}_F$, including $M=0$ and $M=2^n$.

The formula degree lemma supplies the individual bounds $t_i$ and an $O(s)$ point evaluator. Since ${\sum }_i{t}_i\le s$, we have $D=n+{\sum }_i{t}_i\le n+s$; the verifier resource lemma therefore gives $O(s+n)$ field operations including that evaluator.

The soundness theorem gives the stated false-claim error bound with $d_i=t_i$. For a true claim the honest partial sums have these degree bounds, their values at $0,1$ sum to the preceding true value, and their value at each challenge is the next true value. Starting from $M{1}_F$, these identities propagate to the terminal value, so every honest execution accepts.

If $K=M$, their field images are equal, proving the reverse implication. Conversely, equality of the images in ${\mathbb{F}}_p$ implies $p$ divides $K-M$. As $\mathrm{\mid }K-M\mathrm{\mid }\le 2^n<p$, the only possible multiple is zero, so $K=M$. This includes both allowed endpoints for each count. In a field of characteristic $p$ the integer image depends on reduction modulo $p$, regardless of the field cardinality; for example a constant-one formula on one variable has count two and field sum zero in characteristic two.