Internal: AND/OR/NOT Completeness Proof

This internal module proves functional completeness of Basis.unboundedAndOr via DNF (disjunctive normal form) construction. The basis definitions are in Complexitylib.Circuits.AndOrNot.Defs; this module is re-exported through Complexitylib.Circuits.AndOrNot.

def Complexity.AONIndicator {N : ℕ} [NeZero N] (s : BitString N) : Circuit Basis.unboundedAndOr N 1 0

Indicator circuit: outputs true iff the input equals s.

A single N-input AND gate where input i is wired to primary input i, negated when s i = false. No internal gates needed.

Equations

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

def Complexity.andOrNotFor.mkGate {N : ℕ} (f : BitString N → Bool) (i : Fin (2 ^ N)) : Gate Basis.unboundedAndOr (N + 2 ^ N)

DNF circuit computing an arbitrary f : BitString N → Bool.

For each of the 2^N possible inputs s (decoded via Nat.testBit), internal gate i is the indicator AND for s when f s = true, or a trivially-false 0-input OR otherwise. The single output OR gate disjoins all internal gates.

Equations

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

def Complexity.andOrNotFor {N : ℕ} [NeZero N] (f : BitString N → Bool) : Circuit Basis.unboundedAndOr N 1 (2 ^ N)

Single-output DNF circuit computing f : BitString N → Bool.

For each of the 2^N possible inputs s, internal gate i is the indicator AND for s when f s = true, or a trivially-false 0-input OR otherwise. The single output OR gate disjoins all internal gates.

Equations

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

theorem Complexity.andOrNotFor_totalFanIn_le_internal {N : ℕ} [NeZero N] (f : BitString N → Bool) : (andOrNotFor f).totalFanIn ≤ (N + 1) * 2 ^ N

The DNF construction has total fan-in at most (N + 1) * 2^N.

Each of its 2^N internal gates has fan-in either N or zero, and its single output gate has fan-in 2^N.

Helper lemmas for andOrNotFor correctness

theorem Complexity.andOrNotFor_eval {N : ℕ} [NeZero N] (f : BitString N → Bool) : (fun (x : BitString 1) => x 0) ∘ (andOrNotFor f).eval = f

The single-output DNF circuit correctly computes f.

Multi-output DNF circuit: andOrNotForM

def Complexity.andOrNotForM.outIdx {N M : ℕ} (idx : Fin (M * 2 ^ N)) : Fin M

Output coordinate j = idx / 2^N encoded by internal gate index idx of the multi-output DNF circuit.

Equations

• Complexity.andOrNotForM.outIdx idx = ⟨↑idx / 2 ^ N, ⋯⟩

def Complexity.andOrNotForM.rowIdx {N M : ℕ} (idx : Fin (M * 2 ^ N)) : Fin (2 ^ N)

Indicator (truth-table row) coordinate i = idx % 2^N encoded by internal gate index idx of the multi-output DNF circuit.

Equations

• Complexity.andOrNotForM.rowIdx idx = ⟨↑idx % 2 ^ N, ⋯⟩

def Complexity.andOrNotForM.mkGate {N M : ℕ} (f : BitString N → BitString M) (idx : Fin (M * 2 ^ N)) : Gate Basis.unboundedAndOr (N + M * 2 ^ N)

Internal gate idx of the multi-output DNF circuit, with j = outIdx idx and i = rowIdx idx. If output bit j of f on the bit string of i is true, it is an AND indicator gate for row i; otherwise it is a fan-in-0 OR gate, which is constantly false.

Equations

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

def Complexity.andOrNotForM {N M : ℕ} [NeZero N] [NeZero M] (f : BitString N → BitString M) : Circuit Basis.unboundedAndOr N M (M * 2 ^ N)

Multi-output DNF circuit computing f : BitString N → BitString M.

For each output bit j and each of the 2^N possible inputs, there is an indicator AND gate (or a trivially-false gate). Each output OR gate disjoins the 2^N gates for its output bit.

Equations

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

theorem Complexity.andOrNotForM_eval {N M : ℕ} [NeZero N] [NeZero M] (f : BitString N → BitString M) : (andOrNotForM f).eval = f

The multi-output DNF circuit correctly computes f.

instance Complexity.instCompleteBasisUnboundedAndOr : CompleteBasis Basis.unboundedAndOr

Basis.unboundedAndOr is functionally complete: every finite Boolean function f : BitString N → BitString M is computed by some circuit over it, witnessed by the DNF construction andOrNotForM.