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.unboundedAndOr 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.unboundedAndOr 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.

AndOrOp extensions

def Complexity.AndOrOp.dual : AndOrOp → AndOrOp

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

Equations

• Complexity.AndOrOp.and.dual = Complexity.AndOrOp.or
• Complexity.AndOrOp.or.dual = Complexity.AndOrOp.and

def Complexity.AndOrOp.identity : AndOrOp → Bool

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

Equations

• Complexity.AndOrOp.and.identity = true
• Complexity.AndOrOp.or.identity = false

def Complexity.AndOrOp.binOp : AndOrOp → Bool → Bool → Bool

The binary operation corresponding to an AndOrOp.

Equations

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

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

op.eval is the left fold of op.binOp over the inputs, starting from op.identity.

theorem Complexity.AndOrOp.identity_binOp (op : AndOrOp) (b : Bool) : op.binOp op.identity b = b

op.identity is a left identity for op.binOp.

theorem Complexity.AndOrOp.binOp_self (op : AndOrOp) (b : Bool) : op.binOp b b = b

op.binOp is idempotent: op.binOp b b = b.

theorem Complexity.AndOrOp.binOp_assoc (op : AndOrOp) (a b c : Bool) : op.binOp (op.binOp a b) c = op.binOp a (op.binOp b c)

op.binOp is associative.

theorem Complexity.AndOrOp.dual_const (op : AndOrOp) (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 Complexity.AndOrOp.passthrough_eq (op : AndOrOp) (v : Bool) : (op.eval 2 fun (x : Fin 2) => v) = v

A passthrough evaluates to the input value.

theorem Complexity.AndOrOp.eval_zero (op : AndOrOp) : op.eval 0 Fin.elim0 = op.identity

eval on 0 inputs gives the identity.

theorem Complexity.AndOrOp.eval_one (op : AndOrOp) (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 Complexity.CompileAndOr.chainLen (k : ℕ) : ℕ

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

Equations

• Complexity.CompileAndOr.chainLen k = if k ≤ 1 then 1 else k - 1

@[simp]

theorem Complexity.CompileAndOr.chainLen_zero : chainLen 0 = 1

A fan-in-0 gate is simulated by a single (constant) gate.

@[simp]

theorem Complexity.CompileAndOr.chainLen_one : chainLen 1 = 1

A fan-in-1 gate is simulated by a single (passthrough) gate.

theorem Complexity.CompileAndOr.chainLen_pos (k : ℕ) : 0 < chainLen k

Every chain contains at least one gate.

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

For fan-in k ≥ 2, the chain has exactly k - 1 gates.

def Complexity.CompileAndOr.prefixSum (f : ℕ → ℕ) : ℕ → ℕ

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

Equations

• Complexity.CompileAndOr.prefixSum f 0 = 0
• Complexity.CompileAndOr.prefixSum f n.succ = Complexity.CompileAndOr.prefixSum f n + f n

@[simp]

theorem Complexity.CompileAndOr.prefixSum_zero' (f : ℕ → ℕ) : prefixSum f 0 = 0

The empty prefix sum is 0.

theorem Complexity.CompileAndOr.prefixSum_succ (f : ℕ → ℕ) (n : ℕ) : prefixSum f (n + 1) = prefixSum f n + f n

Unfolding lemma: prefixSum f (n + 1) = prefixSum f n + f n.

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

prefixSum f is monotone in the length argument.

Segment lookup

def Complexity.CompileAndOr.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.
• Complexity.CompileAndOr.segLookup 0 f idx h_2 = absurd h_2 ⋯

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

The segment index returned by segLookup is a valid segment number (< n).

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

The position returned by segLookup lies within its segment's size.

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

segLookup decomposes the flat index: segment offset plus position recovers idx.

Wire layout definitions

def Complexity.CompileAndOr.iChainF {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr N M G) (i : ℕ) : ℕ

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

Equations

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

def Complexity.CompileAndOr.oChainF {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr N M G) (j : ℕ) : ℕ

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

Equations

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

def Complexity.CompileAndOr.iTotal {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr N M G) : ℕ

Total number of fan-in-2 gates in all chains simulating internal gates.

Equations

• Complexity.CompileAndOr.iTotal c = Complexity.CompileAndOr.prefixSum (Complexity.CompileAndOr.iChainF c) G

def Complexity.CompileAndOr.oTotal {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr N M G) : ℕ

Total number of fan-in-2 gates in all chains simulating output gates.

Equations

• Complexity.CompileAndOr.oTotal c = Complexity.CompileAndOr.prefixSum (Complexity.CompileAndOr.oChainF c) M

def Complexity.CompileAndOr.G' {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr N M G) : ℕ

Total internal gates in the compiled circuit.

Equations

• Complexity.CompileAndOr.G' c = Complexity.CompileAndOr.iTotal c + Complexity.CompileAndOr.oTotal c

def Complexity.CompileAndOr.iOffset {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr N M G) (i : ℕ) : ℕ

Offset of the chain for internal gate i.

Equations

• Complexity.CompileAndOr.iOffset c i = Complexity.CompileAndOr.prefixSum (Complexity.CompileAndOr.iChainF c) i

def Complexity.CompileAndOr.oOffset {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr N M G) (j : ℕ) : ℕ

Offset of the chain for output gate j.

Equations

• Complexity.CompileAndOr.oOffset c j = Complexity.CompileAndOr.iTotal c + Complexity.CompileAndOr.prefixSum (Complexity.CompileAndOr.oChainF c) j

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

Within bounds, iChainF is the chain length of the corresponding internal gate.

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

Within bounds, oChainF is the chain length of the corresponding output gate.

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

The chain for internal gate i + 1 starts right after the chain for gate i.

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

The chain for internal gate i fits inside the internal-chain region.

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

The chain for output gate j + 1 starts right after the chain for output gate j.

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

The chain for output gate j fits inside the compiled circuit's gate count.

Wire remapping

def Complexity.CompileAndOr.remapWire {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr 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 Complexity.CompileAndOr.remapWire_input {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr N M G) (w : Fin (N + G)) (hw : ↑w < N) : ↑(remapWire c w) = ↑w

remapWire fixes input wires (indices below N).

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

remapWire sends internal gate i to the last gate of its chain.

theorem Complexity.CompileAndOr.remapWire_lt_of_lt {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr 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 Complexity.CompileAndOr.remapWire_lt_oOffset {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr 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 Complexity.CompileAndOr.fin2 {α : Sort u_1} (a b : α) : Fin 2 → α

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

Equations

• Complexity.CompileAndOr.fin2 a b i = if ↑i = 0 then a else b

theorem Complexity.CompileAndOr.fin2_zero {α : Sort u_1} (a b : α) : fin2 a b ⟨0, ⋯⟩ = a

fin2 a b at index 0 is a.

theorem Complexity.CompileAndOr.fin2_one {α : Sort u_1} (a b : α) : fin2 a b ⟨1, ⋯⟩ = b

fin2 a b at index 1 is b.

def Complexity.CompileAndOr.mkChainGate {W : ℕ} (hW : 0 < W) (op : AndOrOp) (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 Complexity.CompileAndOr.compileGates {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr 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 Complexity.CompileAndOr.compileOutputs {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr 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 Complexity.CompileAndOr.compileFn {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr N M G) : Circuit Basis.andOr2 N M (G' c)

The compiled circuit over Basis.andOr2.

Equations

• Complexity.CompileAndOr.compileFn c = { gates := Complexity.CompileAndOr.compileGates c, outputs := Complexity.CompileAndOr.compileOutputs c, acyclic := ⋯ }

Eval equivalence

theorem Complexity.CompileAndOr.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 Complexity.CompileAndOr.wireValue_remapWire {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr 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 Complexity.CompileAndOr.compile_eval {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr N M G) : (compileFn c).eval = c.eval

The compiled fan-in-2 circuit computes the same function as the original circuit.

instance Complexity.instCompleteBasisAndOr2 : CompleteBasis Basis.andOr2

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