Documentation

Complexitylib.Circuits.Schnorr

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 Complexitylib.Circuits.XOR) #

Main results #

The main theorem is schnorr_lower_bound_circuit (proved in the internal descriptor bridge and made available here):

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)) :
    2 * N - 1 ≤ c.size

The hypothesis allows the circuit to compute either XOR or its complement (comp = true for complement). For a single-output circuit, c.size = G + 1, so the bound is equivalently G ≥ 2(N - 1).

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

source
theorem Complexity.schnorr_lower_bound_circuit (N G : ℕ) [NeZero N] (c : Circuit Basis.andOr2 N 1 G) (comp : Bool) (heval : ∀ (x : BitString N), c.eval x 0 = (comp ^^ Schnorr.xorBool N x)) :
2 * N - 1 ≤ c.size

Schnorr's lower bound for circuits: any fan-in-two AND/OR circuit computing N-input parity or its complement has at least 2(N - 1) internal gates. Equivalently, its total size is at least 2N - 1.

source
theorem Complexity.sizeComplexity_xorBool_ge (N : ℕ) [NeZero 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.