Internal: Bridge from CircDesc to Circuit Model

This internal module uses the faithful Circuit-to-CircDesc encoding to transfer descriptor padding and lower bounds to the typed circuit model.

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

Padding

def Complexity.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 Complexity.eval_padDesc {N s s' : ℕ} (d : CircDesc N s) (hs : 0 < s) (h : s ≤ s') (hs' : 0 < s') : CircDesc.eval hs' (padDesc d s' hs h) = CircDesc.eval hs d

Padding preserves evaluation.

Main Theorems

theorem Complexity.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 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)) (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.