Internal: Shannon Upper Bound Construction

The Shannon (1949) upper bound: every Boolean function on N variables can be computed by a fan-in-2 AND/OR circuit of size at most C * 2^N / N, for a fixed constant C and all sufficiently large N.

This is the full-column-library variant (C = 18). The tighter (1 + o(1)) · 2^N / N bound due to Lupanov (1958) uses column grouping and is not yet formalized.

Construction

Split N inputs into k = ⌊log₂ N⌋ - 1 address variables and q = N - k data variables. Decompose any f : {0,1}^N → {0,1} as f(a,y) = ⋁ᵧ [mintermᵧ(data) ∧ colᵧ(addr)] where colᵧ(a) = f(a,y).

Build shared minterm trees for both variable groups, a pattern library for column functions, AND/OR combining layers. Total ≤ 18 · 2^N / N gates for N ≥ 16.

Parameters

def CircuitComplexity.ShannonUpper.addrBits (N : ℕ) : ℕ

Number of address variables: ⌊log₂ N⌋ - 1.

Equations

• CircuitComplexity.ShannonUpper.addrBits N = Nat.log 2 N - 1

def CircuitComplexity.ShannonUpper.dataBits (N : ℕ) : ℕ

Number of data variables: N - addrBits N.

Equations

• CircuitComplexity.ShannonUpper.dataBits N = N - CircuitComplexity.ShannonUpper.addrBits N

Gate Construction Helpers

def CircuitComplexity.ShannonUpper.mkGate2' (op : AONOp) {W : ℕ} (w₀ w₁ : Fin W) (n₀ n₁ : Bool) (bound : ℕ) (hw₀ : ↑w₀ < bound) (hw₁ : ↑w₁ < bound) : { g : Gate Basis.andOr2 W // ∀ (k : Fin g.fanIn), ↑(g.inputs k) < bound }

Build a fan-in-2 gate bundled with an acyclicity proof.

Equations

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

def CircuitComplexity.ShannonUpper.remap₂ (N G₁ G₂ : ℕ) (w : Fin (N + G₂)) : Fin (N + (G₁ + G₂ + 2))

Remap a wire from c₂'s space into the combined space.

Equations

• CircuitComplexity.ShannonUpper.remap₂ N G₁ G₂ w = if h : ↑w < N then ⟨↑w, ⋯⟩ else ⟨↑w + G₁ + 1, ⋯⟩

theorem CircuitComplexity.ShannonUpper.remap₂_val_lt (N G₁ G₂ : ℕ) (w : Fin (N + G₂)) (bound : ℕ) (hb : G₁ + 1 ≤ bound) (hw : ↑w < N + (bound - G₁ - 1)) : ↑(remap₂ N G₁ G₂ w) < N + bound

Remapping a wire preserves its bound in the combined circuit.

def CircuitComplexity.ShannonUpper.gw (idx : ℕ) {W : ℕ} (g : Gate Basis.andOr2 W) : autoParam (idx < 2) gw._auto_1 → Fin W

The wire feeding the selected input of a binary AND/OR gate.

Equations

• CircuitComplexity.ShannonUpper.gw idx g x✝ = g.inputs ⟨idx, ⋯⟩

def CircuitComplexity.ShannonUpper.gn (idx : ℕ) {W : ℕ} (g : Gate Basis.andOr2 W) : autoParam (idx < 2) gn._auto_1 → Bool

Whether the selected input of a binary AND/OR gate is negated.

Equations

• CircuitComplexity.ShannonUpper.gn idx g x✝ = g.negated ⟨idx, ⋯⟩

Binary Circuit Composition

def CircuitComplexity.ShannonUpper.binopGWP {N G₁ G₂ : ℕ} [NeZero N] (c₁ : Circuit Basis.andOr2 N 1 G₁) (c₂ : Circuit Basis.andOr2 N 1 G₂) (i : Fin (G₁ + G₂ + 2)) : { g : Gate Basis.andOr2 (N + (G₁ + G₂ + 2)) // ∀ (k : Fin g.fanIn), ↑(g.inputs k) < N + ↑i }

Gate + acyclicity proof for the binary composition, bundled as a subtype.

Equations

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

def CircuitComplexity.ShannonUpper.binopCircuit (op : AONOp) {N G₁ G₂ : ℕ} [NeZero N] (c₁ : Circuit Basis.andOr2 N 1 G₁) (c₂ : Circuit Basis.andOr2 N 1 G₂) : Circuit Basis.andOr2 N 1 (G₁ + G₂ + 2)

Compose two circuits with a binary AND/OR.

Equations

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

theorem CircuitComplexity.ShannonUpper.binopCircuit_or_correct {N G₁ G₂ : ℕ} [NeZero N] (c₁ : Circuit Basis.andOr2 N 1 G₁) (c₂ : Circuit Basis.andOr2 N 1 G₂) (f₁ f₂ : BitString N → Bool) (hf₁ : (fun (x : BitString N) => c₁.eval x 0) = f₁) (hf₂ : (fun (x : BitString N) => c₂.eval x 0) = f₂) : (fun (x : BitString N) => (binopCircuit AONOp.or c₁ c₂).eval x 0) = fun (x : BitString N) => f₁ x || f₂ x

binopCircuit correctly computes the OR of two circuits' outputs.

The output gate of binopCircuit applies OR to wires N + G₁ and N + G₁ + G₂ + 1, which replicate the output gates of c₁ and c₂. The proof shows that wire values in the combined circuit agree with wire values in the original circuits (via binop_wireValue_c₁ and binop_wireValue_c₂), then combines.

Arithmetic

Nat.log helpers

theorem CircuitComplexity.ShannonUpper.addrBits_ge_three (N : ℕ) (hN : 16 ≤ N) : 3 ≤ addrBits N

theorem CircuitComplexity.ShannonUpper.dataBits_pos (N : ℕ) (hN : 16 ≤ N) : 0 < dataBits N

theorem CircuitComplexity.ShannonUpper.dataBits_ge_two (N : ℕ) (hN : 16 ≤ N) : 2 ≤ dataBits N

Key identities

N² ≤ 2^N for N ≥ 16

Term-by-term bounds

theorem CircuitComplexity.ShannonUpper.shannon_arithmetic (N : ℕ) (hN : 16 ≤ N) : (4 * 2 ^ dataBits N + 2 * 2 ^ addrBits N + 2 ^ (2 ^ addrBits N + addrBits N)) * N ≤ 18 * 2 ^ N

theorem CircuitComplexity.ShannonUpper.shannon_size_le (N : ℕ) (hN : 16 ≤ N) (G : ℕ) (hG : G + 1 ≤ 4 * 2 ^ dataBits N + 2 * 2 ^ addrBits N + 2 ^ (2 ^ addrBits N + addrBits N)) : G + 1 ≤ 18 * 2 ^ N / N

Circuit Construction

Gate construction helper

Circuit layout

def CircuitComplexity.ShannonUpper.szSections (kk qq : ℕ) : ℕ

Total gate count of the Shannon upper-bound circuit construction.

Equations

• CircuitComplexity.ShannonUpper.szSections kk qq = 1 + (2 ^ (qq + 1) - 4) + (2 ^ (kk + 1) - 4) + 2 ^ 2 ^ kk * (2 ^ kk - 1) + 2 ^ qq + (2 ^ qq - 1)

theorem CircuitComplexity.ShannonUpper.szSections_pos (kk qq : ℕ) : 0 < szSections kk qq

Section offsets (not private so they can be unfolded after set)

def CircuitComplexity.ShannonUpper.oC (qq : ℕ) : ℕ

Cumulative gate offset after Section C of the construction.

Equations

• CircuitComplexity.ShannonUpper.oC qq = 1 + (2 ^ (qq + 1) - 4)

def CircuitComplexity.ShannonUpper.oD (kk qq : ℕ) : ℕ

Cumulative gate offset after Section D of the construction.

Equations

• CircuitComplexity.ShannonUpper.oD kk qq = CircuitComplexity.ShannonUpper.oC qq + (2 ^ (kk + 1) - 4)

def CircuitComplexity.ShannonUpper.oE (kk qq : ℕ) : ℕ

Cumulative gate offset after Section E of the construction.

Equations

• CircuitComplexity.ShannonUpper.oE kk qq = CircuitComplexity.ShannonUpper.oD kk qq + 2 ^ 2 ^ kk * (2 ^ kk - 1)

def CircuitComplexity.ShannonUpper.oF (kk qq : ℕ) : ℕ

Cumulative gate offset after Section F of the construction.

Equations

• CircuitComplexity.ShannonUpper.oF kk qq = CircuitComplexity.ShannonUpper.oE kk qq + 2 ^ qq

Power-of-2 helpers

Minterm tree level

def CircuitComplexity.ShannonUpper.treeLevel (j : ℕ) : ℕ

The level (depth from the root) of node j in the selection tree.

Equations

• CircuitComplexity.ShannonUpper.treeLevel j = Nat.log 2 (j + 4) - 1

theorem CircuitComplexity.ShannonUpper.treeLevel_ge_two (j : ℕ) (hj : 4 ≤ j) : 2 ≤ treeLevel j

theorem CircuitComplexity.ShannonUpper.treeLevel_lt (j n : ℕ) (hj : j < 2 ^ (n + 1) - 4) (hn : 2 ≤ n) : treeLevel j < n

def CircuitComplexity.ShannonUpper.treeBase (l : ℕ) : ℕ

The index of the first node at level l of the selection tree.

Equations

• CircuitComplexity.ShannonUpper.treeBase l = 2 ^ (l + 1) - 4

def CircuitComplexity.ShannonUpper.treePos (j l : ℕ) : ℕ

The position of node j within its level of the selection tree.

Equations

• CircuitComplexity.ShannonUpper.treePos j l = j - CircuitComplexity.ShannonUpper.treeBase l

def CircuitComplexity.ShannonUpper.treeParentIdx (l m : ℕ) : ℕ

The index of the parent of a node at level l, position m.

Equations

• CircuitComplexity.ShannonUpper.treeParentIdx l m = CircuitComplexity.ShannonUpper.treeBase (l - 1) + m % 2 ^ l

theorem CircuitComplexity.ShannonUpper.treeBase_le_of_level (j : ℕ) (hj : 4 ≤ j) : treeBase (treeLevel j) ≤ j

theorem CircuitComplexity.ShannonUpper.treeParentIdx_lt_j (l m j : ℕ) (hl : 2 ≤ l) (hm : m = treePos j l) (hbase : treeBase l ≤ j) : treeParentIdx l m < j

Column pattern encoding

noncomputable def CircuitComplexity.ShannonUpper.encodeCol (k : ℕ) (col : Fin (2 ^ k) → Bool) : ℕ

Encode a column of truth-table bits as a natural number.

Equations

• CircuitComplexity.ShannonUpper.encodeCol k col = ∑ j : Fin (2 ^ k), if col j = true then 2 ^ ↑j else 0

theorem CircuitComplexity.ShannonUpper.encodeCol_lt (k : ℕ) (col : Fin (2 ^ k) → Bool) : encodeCol k col < 2 ^ 2 ^ k

noncomputable def CircuitComplexity.ShannonUpper.colFun (N : ℕ) (f : BitString N → Bool) (k q : ℕ) (hkq : k + q = N) (y : Fin (2 ^ q)) : Fin (2 ^ k) → Bool

The Boolean function selecting the addressed column of f. The hypothesis hkq : k + q = N records that the address and data bits partition the inputs.

Equations

• CircuitComplexity.ShannonUpper.colFun N f k q hkq y = fun (a : Fin (2 ^ k)) => f fun (idx : Fin N) => if x : ↑idx < k then (↑a).testBit ↑idx else (↑y).testBit (↑idx - k)

noncomputable def CircuitComplexity.ShannonUpper.colPatIdx (N : ℕ) (f : BitString N → Bool) (k q : ℕ) (hkq : k + q = N) (y : Fin (2 ^ q)) : ℕ

The pattern index of the addressed column of f.

Equations

• CircuitComplexity.ShannonUpper.colPatIdx N f k q hkq y = CircuitComplexity.ShannonUpper.encodeCol k (CircuitComplexity.ShannonUpper.colFun N f k q hkq y)

theorem CircuitComplexity.ShannonUpper.colPatIdx_lt (N : ℕ) (f : BitString N → Bool) (k q : ℕ) (hkq : k + q = N) (y : Fin (2 ^ q)) : colPatIdx N f k q hkq y < 2 ^ 2 ^ k

Shannon gate array

Correctness

colFun reconstruction lemma

Circuit correctness

OR chain induction

The deep wireValue unfolding through all 6 sections (required for
wireValue_andLayer_sem) and the gate array branch analysis make this
the most technically challenging part of the formalization. 

Main correctness theorem

theorem CircuitComplexity.ShannonUpper.shannon_assembly (N : ℕ) [NeZero N] (hN : 16 ≤ N) (f : BitString N → Bool) : ∃ (G : ℕ) (c : Circuit Basis.andOr2 N 1 G), (fun (x : BitString N) => c.eval x 0) = f ∧ G + 1 ≤ 4 * 2 ^ dataBits N + 2 * 2 ^ addrBits N + 2 ^ (2 ^ addrBits N + addrBits N)

Main Theorem

theorem CircuitComplexity.ShannonUpper.shannon_construction (N : ℕ) [NeZero N] (hN : 16 ≤ N) (f : BitString N → Bool) : ∃ (G : ℕ) (c : Circuit Basis.andOr2 N 1 G), (fun (x : BitString N) => c.eval x 0) = f ∧ c.size ≤ 18 * 2 ^ N / N

Shannon circuit construction: For N ≥ 16, every Boolean function has a fan-in-2 AND/OR circuit of size ≤ 18 · 2^N / N.