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 Complexity.ShannonUpper.addrBits (N : ℕ) : ℕ

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

Equations

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

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

Number of data variables: N - addrBits N.

Equations

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

Gate Construction Helpers

def Complexity.ShannonUpper.mkGate2' (op : AndOrOp) {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 Complexity.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

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

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

The input wire at idx of a binary AND/OR gate.

Equations

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

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

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

Equations

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

Binary Circuit Composition

def Complexity.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 Complexity.ShannonUpper.binopCircuit (op : AndOrOp) {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 Complexity.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 AndOrOp.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 Complexity.ShannonUpper.addrBits_ge_three (N : ℕ) (hN : 16 ≤ N) : 3 ≤ addrBits N

For N ≥ 16 there are at least three address variables.

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

For N ≥ 16 there is at least one data variable.

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

For N ≥ 16 there are at least two data variables.

Key identities

N² ≤ 2^N for N ≥ 16

Term-by-term bounds

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

Core counting bound: the total Shannon gate budget times N is at most 18 · 2^N, for N ≥ 16.

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

Any gate count within the Shannon budget is at most 18 · 2^N / N (with the +1 accounting for the output gate), for N ≥ 16.

Circuit Construction

Gate construction helper

Circuit layout

def Complexity.ShannonUpper.totalSectionGates (kk qq : ℕ) : ℕ

Total gate count of the Shannon circuit for kk address and qq data variables: one constant-false gate, the data minterm tree (2^(qq+1) - 4), the address minterm tree (2^(kk+1) - 4), the column library (2^(2^kk) OR chains of length 2^kk - 1), the AND layer (2^qq), and the final OR chain (2^qq - 1).

Equations

• Complexity.ShannonUpper.totalSectionGates kk qq = 1 + (2 ^ (qq + 1) - 4) + (2 ^ (kk + 1) - 4) + 2 ^ 2 ^ kk * (2 ^ kk - 1) + 2 ^ qq + (2 ^ qq - 1)

theorem Complexity.ShannonUpper.totalSectionGates_pos (kk qq : ℕ) : 0 < totalSectionGates kk qq

The Shannon gate array is nonempty.

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

def Complexity.ShannonUpper.addrTreeOffset (qq : ℕ) : ℕ

Gate-index offset of Section C (address minterm tree): after the constant-false gate and the data minterm tree.

Equations

• Complexity.ShannonUpper.addrTreeOffset qq = 1 + (2 ^ (qq + 1) - 4)

def Complexity.ShannonUpper.columnLibraryOffset (kk qq : ℕ) : ℕ

Gate-index offset of Section D (column library): after Section C.

Equations

• Complexity.ShannonUpper.columnLibraryOffset kk qq = Complexity.ShannonUpper.addrTreeOffset qq + (2 ^ (kk + 1) - 4)

def Complexity.ShannonUpper.andLayerOffset (kk qq : ℕ) : ℕ

Gate-index offset of Section E (AND layer): after the column library.

Equations

• Complexity.ShannonUpper.andLayerOffset kk qq = Complexity.ShannonUpper.columnLibraryOffset kk qq + 2 ^ 2 ^ kk * (2 ^ kk - 1)

def Complexity.ShannonUpper.orChainOffset (kk qq : ℕ) : ℕ

Gate-index offset of Section F (final OR chain): after the AND layer.

Equations

• Complexity.ShannonUpper.orChainOffset kk qq = Complexity.ShannonUpper.andLayerOffset kk qq + 2 ^ qq

Power-of-2 helpers

Minterm tree level

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

Level of node j in a minterm tree, where level l occupies indices 2^(l+1) - 4, …, 2^(l+2) - 5: equals ⌊log₂ (j + 4)⌋ - 1.

Equations

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

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

Minterm-tree nodes with index ≥ 4 sit at level 2 or deeper.

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

Nodes within an n-variable minterm tree (index < 2^(n+1) - 4) sit at level < n.

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

Index of the first minterm-tree node at level l: 2^(l+1) - 4.

Equations

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

def Complexity.ShannonUpper.treePosition (j l : ℕ) : ℕ

Position of node j within level l of a minterm tree.

Equations

• Complexity.ShannonUpper.treePosition j l = j - Complexity.ShannonUpper.treeBase l

def Complexity.ShannonUpper.treeParentIndex (l m : ℕ) : ℕ

Index of the parent (at level l - 1) of the level-l node at position m: the parent's level position is m % 2^l.

Equations

• Complexity.ShannonUpper.treeParentIndex l m = Complexity.ShannonUpper.treeBase (l - 1) + m % 2 ^ l

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

Every node with index ≥ 4 lies at or beyond the base of its level.

theorem Complexity.ShannonUpper.treeParentIndex_lt_j (l m j : ℕ) (hl : 2 ≤ l) (hm : m = treePosition j l) (hbase : treeBase l ≤ j) : treeParentIndex l m < j

A minterm-tree node's parent has a strictly smaller index, so tree wiring is acyclic.

Column pattern encoding

noncomputable def Complexity.ShannonUpper.encodeColumn (k : ℕ) (col : Fin (2 ^ k) → Bool) : ℕ

Encode a column function col : Fin (2^k) → Bool as a natural number whose j-th bit is col j; used to index the column pattern library.

Equations

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

theorem Complexity.ShannonUpper.encodeColumn_lt (k : ℕ) (col : Fin (2 ^ k) → Bool) : encodeColumn k col < 2 ^ 2 ^ k

Column encodings are indices into the library of 2^(2^k) patterns.

noncomputable def Complexity.ShannonUpper.columnFunction (N : ℕ) (f : BitString N → Bool) (k q : ℕ) (_hkq : k + q = N) (y : Fin (2 ^ q)) : Fin (2 ^ k) → Bool

The column function of f at data row y: maps an address a to f(a, y), reading the first k input bits from a and the remaining q bits from y.

Equations

• Complexity.ShannonUpper.columnFunction N f k q _hkq y a = f fun (idx : Fin N) => if x : ↑idx < k then (↑a).testBit ↑idx else (↑y).testBit (↑idx - k)

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

Pattern-library index of the column of f at data row y: encodeColumn applied to columnFunction.

Equations

• Complexity.ShannonUpper.columnPatternIndex N f k q hkq y = Complexity.ShannonUpper.encodeColumn k (Complexity.ShannonUpper.columnFunction N f k q hkq y)

theorem Complexity.ShannonUpper.columnPatternIndex_lt (N : ℕ) (f : BitString N → Bool) (k q : ℕ) (hkq : k + q = N) (y : Fin (2 ^ q)) : columnPatternIndex N f k q hkq y < 2 ^ 2 ^ k

Column pattern indices are bounded by the library size 2^(2^k).

Shannon gate array

Correctness

Bit-vector testBit lemma

columnFunction reconstruction lemma

Circuit correctness

Key identity

Connecting the last wire to the OR chain

Semantic decomposition of the circuit

The OR chain accumulates AND-layer semantic values.

This is the key wire-level fact: by induction on r, the OR-chain gate
at position r in Section F evaluates to the foldl-OR of AND-layer
semantic values for y = 0, ..., r+1.

The proof requires tracing wireValue through the gate array, showing:
- The gate at index orChainOffset(k,q) + r is in Section F
- Section F gates are OR gates with inputs pointing to:
  * For r=0: AND gates at andLayerOffset+0 and andLayerOffset+1
  * For r>0: previous OR-chain gate and AND gate at andLayerOffset+(r+1)
- Each AND gate at andLayerOffset+y evaluates to andLayerSem (by wireValue_andLayer_sem)
- The OR of the accumulated value and the new AND output gives
  the extended foldl

The data tree leaf and column library output wire-value proofs
trace wireValue through Sections B and D respectively via
tree-level induction. 

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

Assembled Shannon construction: for N ≥ 16, every Boolean function on N variables has a fan-in-2 AND/OR circuit whose gate count (plus output gate) is within the explicit section-by-section budget.

Main Theorem

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