Schnorr's Lower Bound for XOR Circuits

Any fan-in-2 AND/OR circuit computing the N-input XOR function (or its complement) requires at least 2(N − 1) internal gates.

The proof proceeds by induction on N. At each step:

1. Restrict one input variable, reducing to XOR on N − 1 inputs.
2. Eliminate two gates that become redundant after restriction.
3. Apply the inductive hypothesis to the smaller circuit.

Definitions (from Circ.XOR)

• Schnorr.xorBool N x — the N-input XOR (parity) function

Main results

The main theorem is schnorr_lower_bound_circuit:

theorem schnorr_lower_bound_circuit (N G : Nat) [NeZero N]
    (c : Circuit Basis.andOr2 N 1 G) (comp : Bool)
    (heval : ∀ x, (c.eval x) 0 = comp.xor (Schnorr.xorBool N x))
    (hN : 1 ≤ N) : G + 2 ≥ 2 * N

Here G is the number of internal gates. The hypothesis allows the circuit to compute either XOR or its complement (comp = true for complement). The bound G + 2 ≥ 2 * N means G ≥ 2(N − 1) internal gates, or equivalently G + 1 ≥ 2N − 1 total gates (since Circuit.size = G + 1 for single-output circuits).

When Basis.andOr2 is known to be complete, this yields a sizeComplexity bound via schnorr_size_complexity.

theorem CircuitComplexity.schnorr_size_complexity (N : ℕ) [NeZero N] (hN : 1 ≤ N) [CompleteBasis Basis.andOr2] : Circuit.sizeComplexity Basis.andOr2 (Schnorr.xorBool N) ≥ 2 * N - 1

Schnorr lower bound in terms of sizeComplexity: the fan-in-2 AND/OR circuit complexity of N-input XOR is at least 2N − 1.