Internal: Schnorr's Lower Bound for XOR Circuits

This internal module proves Schnorr's lower bound via the CircDesc model. The public definitions (Schnorr.xorBool, Schnorr.xorBool_flip, Schnorr.xorBool_essential) are in Circ.XOR. The public theorem schnorr_lower_bound_circuit is accessible through Circ.Schnorr.

def CircuitComplexity.Schnorr.insertAt {N : ℕ} (x : BitString N) (a : Fin (N + 1)) (b : Bool) : BitString (N + 1)

Insert value b at position a in a BitString.

Equations

• CircuitComplexity.Schnorr.insertAt x a b j = if h1 : ↑j < ↑a then x ⟨↑j, ⋯⟩ else if h2 : ↑j = ↑a then b else x ⟨↑j - 1, ⋯⟩

theorem CircuitComplexity.Schnorr.xorBool_insertAt {N : ℕ} (x : BitString N) (a : Fin (N + 1)) (b : Bool) : xorBool (N + 1) (insertAt x a b) = (b ^^ xorBool N x)

XOR with an inserted bit equals the inserted bit XORed with XOR of the rest.

CircDesc Insensitivity

theorem CircuitComplexity.Schnorr.wireValD_eq_of_unreferenced {N s : ℕ} (d : CircDesc N s) (a : Fin N) (b : Bool) (hno : ∀ (g : Fin s), ↑(d g).2.1.1 ≠ ↑a ∧ ↑(d g).2.1.2 ≠ ↑a) (x : BitString N) (w : Fin (N + s)) (hw : ↑w ≠ ↑a) : wireValD d x w = wireValD d (Function.update x a b) w

If no gate references input a, wire values are unchanged when a is modified.

theorem CircuitComplexity.Schnorr.evalD_essential_means_referenced {N s : ℕ} (d : CircDesc N s) (hs : 0 < s) (a : Fin N) (hdep : ∃ (x : BitString N), evalD hs d x ≠ evalD hs d (Function.update x a !x a)) : ∃ (g : Fin s), ↑(d g).2.1.1 = ↑a ∨ ↑(d g).2.1.2 = ↑a

If evaluation depends on input a, some gate references a.

Circuit Restriction

def CircuitComplexity.Schnorr.remapWireR {N s : ℕ} (a : Fin (N + 1)) (b : Bool) (g : Fin s) (wi : Fin (N + 1 + s)) (ni : Bool) : Fin (N + s) × Bool

Remap a wire reference when fixing input a.

Equations

• CircuitComplexity.Schnorr.remapWireR a b g wi ni = if h1 : ↑wi = ↑a then (⟨N + ↑g, ⋯⟩, ni ^^ b) else if h2 : ↑wi < ↑a then (⟨↑wi, ⋯⟩, ni) else (⟨↑wi - 1, ⋯⟩, ni)

def CircuitComplexity.Schnorr.restrictD {N s : ℕ} (d : CircDesc (N + 1) s) (a : Fin (N + 1)) (b : Bool) : CircDesc N s

Fix primary input a of a CircDesc (N+1) s to value b.

Equations

• One or more equations did not get rendered due to their size.

theorem CircuitComplexity.Schnorr.evalD_restrictD {N s : ℕ} (d : CircDesc (N + 1) s) (hs : 0 < s) (a : Fin (N + 1)) (b : Bool) (x : BitString N) : evalD hs (restrictD d a b) x = evalD hs d (insertAt x a b)

Gate Elimination

inductive CircuitComplexity.Schnorr.GateRedirect (W : ℕ) : Type

How to redirect references to an eliminated gate.

• const {W : ℕ} (c : Bool) : GateRedirect W
• wire {W : ℕ} (w : Fin W) (flip : Bool) : GateRedirect W

def CircuitComplexity.Schnorr.remapWireE {N s : ℕ} (g : Fin (s + 1)) (rd : GateRedirect (N + s)) (i : Fin s) (wi : Fin (N + (s + 1))) (ni : Bool) : Fin (N + s) × Bool

Remap a wire reference when eliminating gate g.

Equations

• One or more equations did not get rendered due to their size.

def CircuitComplexity.Schnorr.elimGateD {N s : ℕ} (d : CircDesc N (s + 1)) (g : Fin (s + 1)) (rd : GateRedirect (N + s)) : CircDesc N s

Remove gate g from a CircDesc, redirecting references to it.

Equations

• One or more equations did not get rendered due to their size.

theorem CircuitComplexity.Schnorr.evalD_elimGateD {N s : ℕ} (d : CircDesc N (s + 1)) (hs : 0 < s) (g : Fin (s + 1)) (rd : GateRedirect (N + s)) (hrd : ∀ (x : BitString N), wireValD d x ⟨N + ↑g, ⋯⟩ = match rd with | GateRedirect.const c => c | GateRedirect.wire w flip => flip ^^ wireValD d x ⟨↑w, ⋯⟩) (hrd_wire : ∀ (w' : Fin (N + s)) (flip : Bool), rd = GateRedirect.wire w' flip → ↑w' < N + ↑g) (hg_not_last : ↑g < s) (x : BitString N) : evalD hs (elimGateD d g rd) x = evalD ⋯ d x

Restriction eliminates two gates

XOR needs ≥ 3 gates

theorem CircuitComplexity.Schnorr.restriction_eliminates_two {n s : ℕ} (d : CircDesc (n + 1) s) (hs : 0 < s) (hn : 0 < n) (comp : Bool) (heval : ∀ (x : BitString (n + 1)), evalD hs d x = (comp ^^ xorBool (n + 1) x)) (hessential : ∀ (a : Fin (n + 1)) (x : BitString (n + 1)), evalD hs d x ≠ evalD hs d (Function.update x a !x a)) : ∃ (s' : ℕ) (d' : CircDesc n s') (hs' : 0 < s') (comp' : Bool), s' + 2 ≤ s ∧ ∀ (x : BitString n), evalD hs' d' x = (comp' ^^ xorBool n x)

Key inductive step: restricting one variable of a totally essential XOR circuit yields a circuit for XOR on one fewer input, with at least 2 fewer gates.

The 2(N-1) Lower Bound

theorem CircuitComplexity.Schnorr.xor_lower_bound_2 (N s : ℕ) (hs : 0 < s) (d : CircDesc N s) (comp : Bool) (heval : ∀ (x : BitString N), evalD hs d x = (comp ^^ xorBool N x)) (hN : 1 ≤ N) : s + 1 ≥ 2 * N

Any DeMorgan circuit computing XOR_N (or complement) has ≥ 2N - 1 gates.