Parity in TC0

Circuit.thresholdParity N computes N-input parity (Schnorr.xorBool) with N unweighted threshold gates of fan-in N, one output threshold gate, and depth two. Collecting these circuits into a family shows that parity lies in the nonuniform class TC0: polynomial-size, constant-depth threshold circuits with free negation on gate inputs.

theorem Complexity.xorBool_eq_decide_countP (N : ℕ) (x : BitString N) : Schnorr.xorBool N x = decide (Fin.countP x % 2 = 1)

Parity is the parity of the number of true inputs.

theorem Complexity.Circuit.eval_thresholdParity (N : ℕ) [NeZero N] (x : BitString N) : (thresholdParity N).eval x 0 = Schnorr.xorBool N x

The depth-two threshold circuit computes parity.

theorem Complexity.Circuit.size_thresholdParity (N : ℕ) [NeZero N] : (thresholdParity N).size = N + 1

The parity circuit has N internal gates and one output gate.

theorem Complexity.Circuit.depth_thresholdParity_le (N : ℕ) [NeZero N] : (thresholdParity N).depth ≤ 2

The parity circuit has depth at most two.

theorem Complexity.CircuitFamily.thresholdParity_computes : thresholdParity.Computes Schnorr.xorBool

The threshold parity family computes parity at every length, including the empty input.

theorem Complexity.CircuitFamily.thresholdParity_sizeBoundedBy : thresholdParity.SizeBoundedBy fun (n : ℕ) => n + 1

The threshold parity family has size at most n + 1 at length n.

theorem Complexity.CircuitFamily.thresholdParity_depthBoundedBy : thresholdParity.DepthBoundedBy fun (x : ℕ) => 2

The threshold parity family has depth at most two at every length.

theorem Complexity.xorBool_mem_TC0 : Schnorr.xorBool ∈ TC0

Parity is in TC0. The parity family is computed by polynomial-size, constant-depth, unbounded-fan-in threshold circuits.