Check if n-bit number is divisible by 7

$8^k \cdot x \mod 7 = x \mod 7$, therefore we can split the number into groups of three bits and add these groups.

Now you use a 3-2 adder: A 3-2 adder takes three n-bit inputs and creates one n-bit output and one n-bit shifted output with the same sum: This is just done by connecting all triples of three bits with a one-bit full adder.

Now if you add three 3-bit values with bit values 421, 421 and 421, and get two sums 421 and 842, then 8 mod 7 = 1, so you move the bit at index 3 to index 0, and you turned three 3-bit numbers into two 3-bit numbers with the same value modulo 7.

Say you have a 128 bit number. Split into 43 3 bit numbers. Add 3 numbers, 14 times in parallel, and you have 28+1 = 29 numbers. Then add 9 times 3 numbers, and get 20 numbers. Add 6 times 3 numbers, getting 14 numbers, then from 14 to 10, from 10 to 7, from 7 to 5, from 5 to 4, from 4 to 3, and finally from 3 to two 3-bit numbers.

That sum x+y is divisible by 7 if x xor y is all bits zero or all bits 1.

The set of all numbers divisible by $7$ is regular: it can be decided by a simple $7$-state finite automaton that keeps track of the remainder modulo $7$ of the number seen so far. Now, every regular language $L$ (say, over the binary alphabet) is computable by a (DLOGTIME-uniform) family of log-depth circuits:

Fix a DFA $(Q,\delta,q_0,F)$ for $L$, and by induction on $n$, construct formulas $\phi_{n,q,r}(x_0,\dots,x_{n-1})$ of depth $O(\log n)$ for $n\in\mathbb N$ and $q,r\in Q$, expressing that the input $x_0\dots x_{n-1}$ takes the automaton from state $q$ to state $r$:

• $\phi_{0,q,r}$ is constant $1$ or $0$ depending on whether $q=r$;
• $\phi_{1,q,r}(x_0)$ is one of $1$, $0$, $x_0$, or $\neg x_0$ according to whether $\delta(q,0)=r$ and/or $\delta(q,1)=r$;
• for $n>1$, define $\phi_{n,q,r}(x_0,\dots,x_{n-1})$ recursively as $$\bigvee_{s\in Q}\bigl(\phi_{\lceil n/2\rceil,q,s}(x_0,\dots,x_{\lceil n/2\rceil-1})\land\phi_{\lfloor n/2\rfloor,s,r}(x_{\lceil n/2\rceil},\dots,x_{n-1})\bigr).$$

Finally, $x\in L$ is for $|x|=n$ decided by the formula $$\bigvee_{q\in F}\phi_{n,q_0,q}(x_0,\dots,x_{n-1}).$$