Internal: Bridge from CircDesc to Circuit Model

This internal module connects the CircDesc counting model to the general Circuit model by proving that circuits over Basis.andOr2 encode faithfully into circuit descriptors.

The public theorems shannon_lower_bound_circuit and schnorr_lower_bound_circuit are accessible through Circ.Shannon and Circ.Schnorr respectively.

Encoding

def CircuitComplexity.encodeGate {W W' : ℕ} (g : Gate Basis.andOr2 W) (hW : W ≤ W') : GateSlot W'

Encode a Basis.andOr2 gate as a GateSlot.

Equations

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

def CircuitComplexity.circuitToDesc {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) : CircDesc N (G + 1)

Encode a circuit over Basis.andOr2 as a circuit descriptor. Internal gates map to positions 0..G-1; the output gate to position G.

Equations

• CircuitComplexity.circuitToDesc c i = if h : ↑i < G then CircuitComplexity.encodeGate (c.gates ⟨↑i, h⟩) ⋯ else CircuitComplexity.encodeGate (c.outputs 0) ⋯

Semantic Equivalence

theorem CircuitComplexity.wireValue_eq_wireValD {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) (input : BitString N) (w : Fin (N + G)) : c.wireValue input w = wireValD (circuitToDesc c) input ⟨↑w, ⋯⟩

Wire values agree between Circuit.wireValue and wireValD for wires in the range 0..N+G-1.

theorem CircuitComplexity.circuit_eval_eq_evalD {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) : (fun (x : BitString N) => c.eval x 0) = evalD ⋯ (circuitToDesc c)

Circuit evaluation agrees with descriptor evaluation.

Padding

def CircuitComplexity.padDesc {N s : ℕ} (d : CircDesc N s) (s' : ℕ) (hs : 0 < s) (h : s ≤ s') : CircDesc N s'

Pad a descriptor to a larger size by appending copy gates. Each padded gate is OR(last_output, last_output) which copies the original output value.

Equations

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

theorem CircuitComplexity.evalD_padDesc {N s s' : ℕ} (d : CircDesc N s) (hs : 0 < s) (h : s ≤ s') (hs' : 0 < s') : evalD hs' (padDesc d s' hs h) = evalD hs d

Padding preserves evaluation.

Main Theorems

theorem CircuitComplexity.shannon_lower_bound_circuit (N : ℕ) [NeZero N] (hN : 6 ≤ N) : ∃ (f : BitString N → Bool), ∀ (G : ℕ) (c : Circuit Basis.andOr2 N 1 G), G + 1 ≤ 2 ^ N / (5 * N) → (fun (x : BitString N) => c.eval x 0) ≠ f

Shannon lower bound for circuits: for N ≥ 6, there exists a Boolean function on N inputs that cannot be computed by any fan-in-2 AND/OR circuit of size at most 2^N/(5N).

theorem CircuitComplexity.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)) (hN : 1 ≤ N) : G + 2 ≥ 2 * N

Schnorr's lower bound for circuits: any fan-in-2 AND/OR circuit computing XOR_N (or its complement) has at least 2(N-1) internal gates, i.e., G + 1 (total gates including output) ≥ 2N - 1.