Internal: Completeness of fan-in-2 AND/OR

This module proves CompleteBasis Basis.andOr2 using the generic simulation lemma CompleteBasis.of_simulation. The proof compiles any circuit over Basis.unboundedAON into one over Basis.andOr2 by decomposing each unbounded fan-in gate into a chain of fan-in-2 gates.

Strategy

Given a circuit c : Circuit Basis.unboundedAON N M G, we construct c' : Circuit Basis.andOr2 N M G' with c'.eval = c.eval.

Each original gate with fan-in k is replaced by a chain of chainLen k fan-in-2 gates:

• k = 0: one constant gate (dual-op trick: OR(x₀, ¬x₀) = true, etc.)
• k = 1: one passthrough gate (op(x₀, x₀) = x₀)
• k ≥ 2: k - 1 gates chaining the inputs left-to-right

The new circuit's internal gates consist of chains for all original internal gates followed by chains for all original output gates. The new output gates are trivial passthroughs reading the last wire of each output chain.

AONOp extensions

def CircuitComplexity.AONOp.dual : AONOp → AONOp

Dual operation: swaps AND ↔ OR. Used for constant-gate construction.

Equations

• CircuitComplexity.AONOp.and.dual = CircuitComplexity.AONOp.or
• CircuitComplexity.AONOp.or.dual = CircuitComplexity.AONOp.and

def CircuitComplexity.AONOp.identity : AONOp → Bool

Identity element for fold: true for AND, false for OR.

Equations

• CircuitComplexity.AONOp.and.identity = true
• CircuitComplexity.AONOp.or.identity = false

def CircuitComplexity.AONOp.binOp : AONOp → Bool → Bool → Bool

The binary operation corresponding to an AONOp.

Equations

• CircuitComplexity.AONOp.and.binOp = fun (x1 x2 : Bool) => x1 && x2
• CircuitComplexity.AONOp.or.binOp = fun (x1 x2 : Bool) => x1 || x2

theorem CircuitComplexity.AONOp.eval_eq_foldl (op : AONOp) (n : ℕ) (v : BitString n) : op.eval n v = Fin.foldl n (fun (acc : Bool) (i : Fin n) => op.binOp acc (v i)) op.identity

theorem CircuitComplexity.AONOp.identity_binOp (op : AONOp) (b : Bool) : op.binOp op.identity b = b

theorem CircuitComplexity.AONOp.binOp_self (op : AONOp) (b : Bool) : op.binOp b b = b

theorem CircuitComplexity.AONOp.binOp_assoc (op : AONOp) (a b c : Bool) : op.binOp (op.binOp a b) c = op.binOp a (op.binOp b c)

theorem CircuitComplexity.AONOp.dual_const (op : AONOp) (b : Bool) : (op.dual.eval 2 fun (i : Fin 2) => (if ↑i = 0 then false else true) ^^ b) = op.identity

The dual-op trick for constants: OR(b, ¬b) = true, AND(b, ¬b) = false.

theorem CircuitComplexity.AONOp.passthrough_eq (op : AONOp) (v : Bool) : (op.eval 2 fun (x : Fin 2) => v) = v

A passthrough evaluates to the input value.

theorem CircuitComplexity.AONOp.eval_zero (op : AONOp) : op.eval 0 Fin.elim0 = op.identity

eval on 0 inputs gives the identity.

theorem CircuitComplexity.AONOp.eval_one (op : AONOp) (v : Fin 1 → Bool) : op.eval 1 v = op.binOp op.identity (v 0)

eval on 1 input gives identity op input.

Chain length and prefix sums

def CircuitComplexity.CompileAON.chainLen (k : ℕ) : ℕ

Number of fan-in-2 gates needed to simulate one gate with k inputs.

Equations

• CircuitComplexity.CompileAON.chainLen k = if k ≤ 1 then 1 else k - 1

@[simp]

theorem CircuitComplexity.CompileAON.chainLen_zero : chainLen 0 = 1

@[simp]

theorem CircuitComplexity.CompileAON.chainLen_one : chainLen 1 = 1

theorem CircuitComplexity.CompileAON.chainLen_pos (k : ℕ) : 0 < chainLen k

theorem CircuitComplexity.CompileAON.chainLen_of_ge_two {k : ℕ} (hk : 2 ≤ k) : chainLen k = k - 1

def CircuitComplexity.CompileAON.prefixSum (f : ℕ → ℕ) : ℕ → ℕ

Prefix sum: prefixSum f n = f 0 + f 1 + ⋯ + f (n-1).

Equations

• CircuitComplexity.CompileAON.prefixSum f 0 = 0
• CircuitComplexity.CompileAON.prefixSum f n.succ = CircuitComplexity.CompileAON.prefixSum f n + f n

@[simp]

theorem CircuitComplexity.CompileAON.prefixSum_zero' (f : ℕ → ℕ) : prefixSum f 0 = 0

theorem CircuitComplexity.CompileAON.prefixSum_succ (f : ℕ → ℕ) (n : ℕ) : prefixSum f (n + 1) = prefixSum f n + f n

theorem CircuitComplexity.CompileAON.prefixSum_mono (f : ℕ → ℕ) {i j : ℕ} (h : i ≤ j) : prefixSum f i ≤ prefixSum f j

Segment lookup

def CircuitComplexity.CompileAON.segLookup (n : ℕ) (f : ℕ → ℕ) (idx : ℕ) (h : idx < prefixSum f n) : ℕ × ℕ

Given a flat index into a segmented array, find the segment and position.

Equations

• One or more equations did not get rendered due to their size.
• CircuitComplexity.CompileAON.segLookup 0 f idx h_2 = absurd h_2 ⋯

theorem CircuitComplexity.CompileAON.segLookup_fst_lt (n : ℕ) (f : ℕ → ℕ) (idx : ℕ) (h : idx < prefixSum f n) : (segLookup n f idx h).1 < n

theorem CircuitComplexity.CompileAON.segLookup_snd_lt (n : ℕ) (f : ℕ → ℕ) (idx : ℕ) (h : idx < prefixSum f n) : (segLookup n f idx h).2 < f (segLookup n f idx h).1

theorem CircuitComplexity.CompileAON.segLookup_sum (n : ℕ) (f : ℕ → ℕ) (idx : ℕ) (h : idx < prefixSum f n) : prefixSum f (segLookup n f idx h).1 + (segLookup n f idx h).2 = idx

Wire layout definitions

def CircuitComplexity.CompileAON.iChainF {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) (i : ℕ) : ℕ

Chain size function for internal gates (0-padded beyond G).

Equations

• CircuitComplexity.CompileAON.iChainF c i = if h : i < G then CircuitComplexity.CompileAON.chainLen (c.gates ⟨i, h⟩).fanIn else 0

def CircuitComplexity.CompileAON.oChainF {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) (j : ℕ) : ℕ

Chain size function for output gates (0-padded beyond M).

Equations

• CircuitComplexity.CompileAON.oChainF c j = if h : j < M then CircuitComplexity.CompileAON.chainLen (c.outputs ⟨j, h⟩).fanIn else 0

def CircuitComplexity.CompileAON.iTotal {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) : ℕ

Total number of compiled gates contributed by the internal gates.

Equations

• CircuitComplexity.CompileAON.iTotal c = CircuitComplexity.CompileAON.prefixSum (CircuitComplexity.CompileAON.iChainF c) G

def CircuitComplexity.CompileAON.oTotal {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) : ℕ

Total number of compiled gates contributed by the output gates.

Equations

• CircuitComplexity.CompileAON.oTotal c = CircuitComplexity.CompileAON.prefixSum (CircuitComplexity.CompileAON.oChainF c) M

def CircuitComplexity.CompileAON.G' {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) : ℕ

Total internal gates in the compiled circuit.

Equations

• CircuitComplexity.CompileAON.G' c = CircuitComplexity.CompileAON.iTotal c + CircuitComplexity.CompileAON.oTotal c

def CircuitComplexity.CompileAON.iOffset {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) (i : ℕ) : ℕ

Offset of the chain for internal gate i.

Equations

• CircuitComplexity.CompileAON.iOffset c i = CircuitComplexity.CompileAON.prefixSum (CircuitComplexity.CompileAON.iChainF c) i

def CircuitComplexity.CompileAON.oOffset {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) (j : ℕ) : ℕ

Offset of the chain for output gate j.

Equations

• CircuitComplexity.CompileAON.oOffset c j = CircuitComplexity.CompileAON.iTotal c + CircuitComplexity.CompileAON.prefixSum (CircuitComplexity.CompileAON.oChainF c) j

theorem CircuitComplexity.CompileAON.iChainF_eq {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) {i : ℕ} (hi : i < G) : iChainF c i = chainLen (c.gates ⟨i, hi⟩).fanIn

theorem CircuitComplexity.CompileAON.oChainF_eq {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) {j : ℕ} (hj : j < M) : oChainF c j = chainLen (c.outputs ⟨j, hj⟩).fanIn

theorem CircuitComplexity.CompileAON.iOffset_succ {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) {i : ℕ} (hi : i < G) : iOffset c (i + 1) = iOffset c i + chainLen (c.gates ⟨i, hi⟩).fanIn

theorem CircuitComplexity.CompileAON.iOffset_chain_le_iTotal {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) {i : ℕ} (hi : i < G) : iOffset c i + chainLen (c.gates ⟨i, hi⟩).fanIn ≤ iTotal c

theorem CircuitComplexity.CompileAON.oOffset_succ {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) {j : ℕ} (hj : j < M) : oOffset c (j + 1) = oOffset c j + chainLen (c.outputs ⟨j, hj⟩).fanIn

theorem CircuitComplexity.CompileAON.oOffset_chain_le_G' {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) {j : ℕ} (hj : j < M) : oOffset c j + chainLen (c.outputs ⟨j, hj⟩).fanIn ≤ G' c

Wire remapping

def CircuitComplexity.CompileAON.remapWire {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) (w : Fin (N + G)) : Fin (N + G' c)

Map an old wire index to its new position. Input wires are unchanged; internal gate i maps to the last gate of its chain.

Equations

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

theorem CircuitComplexity.CompileAON.remapWire_input {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) (w : Fin (N + G)) (hw : ↑w < N) : ↑(remapWire c w) = ↑w

theorem CircuitComplexity.CompileAON.remapWire_gate {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) {i : ℕ} (hi : i < G) : ↑(remapWire c ⟨N + i, ⋯⟩) = N + iOffset c i + chainLen (c.gates ⟨i, hi⟩).fanIn - 1

theorem CircuitComplexity.CompileAON.remapWire_lt_of_lt {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) (w : Fin (N + G)) {i : ℕ} (hi : i ≤ G) (hw : ↑w < N + i) : ↑(remapWire c w) < N + iOffset c i

If w < N + i in the old circuit, remapWire w < N + iOffset i in the new.

theorem CircuitComplexity.CompileAON.remapWire_lt_oOffset {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) (w : Fin (N + G)) (j : ℕ) : ↑(remapWire c w) < N + oOffset c j

remapWire maps to a wire that comes before any output chain.

Chain gate construction

def CircuitComplexity.CompileAON.fin2 {α : Sort u_1} (a b : α) : Fin 2 → α

Helper: construct a function Fin 2 → α from two values.

Equations

• CircuitComplexity.CompileAON.fin2 a b i = if ↑i = 0 then a else b

@[simp]

theorem CircuitComplexity.CompileAON.fin2_zero {α : Sort u_1} (a b : α) : fin2 a b 0 = a

@[simp]

theorem CircuitComplexity.CompileAON.fin2_one {α : Sort u_1} (a b : α) : fin2 a b 1 = b

def CircuitComplexity.CompileAON.mkChainGate {W : ℕ} (hW : 0 < W) (op : AONOp) (k : ℕ) (ri : Fin k → Fin W) (rn : Fin k → Bool) (base j : ℕ) (hj : j < chainLen k) (hbase : base + chainLen k ≤ W) : Gate Basis.andOr2 W

Build the j-th fan-in-2 gate in a chain for an original gate. Components are split out so projections reduce without unfolding dite.

Equations

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

Compiled circuit

def CircuitComplexity.CompileAON.compileGates {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) (idx : Fin (G' c)) : Gate Basis.andOr2 (N + G' c)

Gate function for the compiled circuit. Components are separated so projections reduce without going through dite.

Equations

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

def CircuitComplexity.CompileAON.compileOutputs {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) (j : Fin M) : Gate Basis.andOr2 (N + G' c)

Output gates: passthroughs reading the last wire of each output chain.

Equations

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

def CircuitComplexity.CompileAON.compileFn {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) : Circuit Basis.andOr2 N M (G' c)

The compiled circuit over Basis.andOr2.

Equations

• CircuitComplexity.CompileAON.compileFn c = { gates := CircuitComplexity.CompileAON.compileGates c, outputs := CircuitComplexity.CompileAON.compileOutputs c, acyclic := ⋯ }

Eval equivalence

theorem CircuitComplexity.CompileAON.segLookup_of_prefixSum (n : ℕ) (f : ℕ → ℕ) (i j : ℕ) (hi : i < n) (hj : j < f i) (h : prefixSum f i + j < prefixSum f n) : segLookup n f (prefixSum f i + j) h = (i, j)

segLookup inverts prefixSum: if idx = prefixSum f i + j and j < f i, then segLookup returns (i, j).

theorem CircuitComplexity.CompileAON.wireValue_remapWire {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) (input : BitString N) (w : Fin (N + G)) : (compileFn c).wireValue input (remapWire c w) = c.wireValue input w

Key lemma: remapWire values in the compiled circuit match the original.

theorem CircuitComplexity.CompileAON.compile_eval {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAON N M G) : (compileFn c).eval = c.eval

instance CircuitComplexity.instCompleteBasisAndOr2 : CompleteBasis Basis.andOr2

Fan-in-2 AND/OR is functionally complete.