# Parity is not in QAC<sup>0</sup>

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Product-projection localization and the $\mathrm{QAC}^0$ parity lower bound](../../preprints/Product-projection-localization-and-the-QAC0-parity-lower-bound-September-24-2026/paper.pdf)
- [Regular trajectories, pruning and quantum parity](../../preprints/Regular-trajectories-pruning-and-quantum-parity-September-24-2026/paper.pdf)

## Scope

The formalization rules out bounded-error parity computation by constant-depth quantum circuits with polynomially many zero-initialized ancillary qubits. For every fixed depth, polynomial bound on the total number of qubits, and $0<\varepsilon\le1/2$, every sufficiently large input length has an input on which the measured-output parity success probability is less than $1/2+\varepsilon$. A companion specialization gives success strictly below $2/3$. The formalization also includes the product-projection localization estimate supporting this bound.

The formalized result supplies the polynomial-size parity consequence of the paper. For every fixed circuit depth and polynomial bound on the number of qubits, all sufficiently large input lengths have an input on which any such circuit computes measured-output parity with probability strictly below $2/3$. Ancillary qubits start at zero. The formalization also contains the general positive-advantage parity bound and its product-projection localization estimate; regular-trajectory propagation and pruning are not separate formalized statements here.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Constant-depth quantum parity lower bound | [QACParity.lean](../ComparatorChallenges/QACParity.lean) |
| Polynomial-size parity specialization | [RegularParity.lean](../ComparatorChallenges/RegularParity.lean) |
| Polynomial-size quantum parity lower bound | [RegularParity.lean](../ComparatorChallenges/RegularParity.lean) |
| General positive-advantage parity lower bound | [QACParity.lean](../ComparatorChallenges/QACParity.lean) |