Let $CC^0[m]$ be the class of constant-depth, polynomial-sized circuits consisting entirely of $MOD_m$ gates, which put out $1$ iff the sum of their inputs $\equiv 0~(\textrm{mod}~m)$. In the same way that $DLOGTIME$-uniform $AC^0$ is equivalent to $FO[<,bit] = FO[+,*]$, in multiple sources 1, 2 it's asserted that $DLOGTIME$-uniform $CC^0$ is equivalent to $MOD[+,*]$, the set of logical sentences using only the modular quantifier $\exists^{(m,k)}$ that evaluates to true iff the number of satisfying solutions is congruent to $k$ mod $m$.
However, all of the sources that are cited for these claims 3, [4], [5] only provide proofs for the classes $AC^0, ACC^0, TC^0, NC^1$ and rely on the usage of standard quantifiers $\forall, \exists$, which are not proven to be expressible in $CC^0$. Does anyone know of how to modify the original proofs of $DLOGTIME-AC^0 = FO[<,bit] = FO[+,*]$ to achieve $DLOGTIME-CC^0 = MOD[<,bit] = MOD[+,*]$ without using these quantifiers, or a source for such proofs?
[4]: Introduction to Circuit Complexity: A Uniform Approach by Heribert Vollmer
[5]: Descriptive Complexity by Neil Immerman
(These proofs mostly just follow the one laid out in 3)
