MOD3 binary divisibility problem ($\{x:{\mathrm{value}}_2(x)\equiv 0(\mathrm{mod}3)\}$)

For a binary numeral, its remainder is the sum of its bits weighted alternately by $+1$ and $-1$ from the least significant position. A balanced finite-monoid reduction circuit adds these residues modulo three in two-bit encodings. A final zero test gives a uniform linear-size logarithmic-depth Boolean circuit, proving membership in NC1.