Parity is not in AC0 -- proof internals #
The family-level argument instantiates the finite counting obstruction
AC0Formula.parity_counting_obstruction. A polynomial-size family of depth at
most c normalizes, at each length N, to a parity formula of depth at most c
and size at most B * N ^ K. With d = c + 1 stages, query depth
s = (d + 1) * K + d + 1, and length N = m ^ (d + 1) for one explicit large
m, taking q = m makes both right-hand terms of the obstruction smaller than
half of its left-hand side.