Internal: AND/OR/NOT Completeness Proof

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

def CircuitComplexity.AONIndicator {N : ℕ} [NeZero N] (s : BitString N) : Circuit Basis.unboundedAON 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 CircuitComplexity.AONFor.mkGate {N : ℕ} (f : BitString N → Bool) (i : Fin (2 ^ N)) : Gate Basis.unboundedAON (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 CircuitComplexity.AONFor {N : ℕ} [NeZero N] (f : BitString N → Bool) : Circuit Basis.unboundedAON 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.

Helper lemmas for AONFor correctness

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

The single-output DNF circuit correctly computes f.

Multi-output DNF circuit: AONForM

def CircuitComplexity.aonOutputIndex {N M : ℕ} (idx : Fin (M * 2 ^ N)) : Fin M

Internal gate for the multi-output DNF circuit. Gate idx encodes output bit j = idx / 2^N and indicator index i = idx % 2^N. If f(bitstring i)[j] = true, it's an AND indicator gate; otherwise a trivially-false OR gate.

Equations

• CircuitComplexity.aonOutputIndex idx = ⟨↑idx / 2 ^ N, ⋯⟩

def CircuitComplexity.aonInputIndex {N M : ℕ} (idx : Fin (M * 2 ^ N)) : Fin (2 ^ N)

The input assignment index encoded by a gate position.

Equations

• CircuitComplexity.aonInputIndex idx = ⟨↑idx % 2 ^ N, ⋯⟩

def CircuitComplexity.aonGate {N M : ℕ} (f : BitString N → BitString M) (idx : Fin (M * 2 ^ N)) : Gate Basis.unboundedAON (N + M * 2 ^ N)

The conjunction gate for an output coordinate and an input assignment.

Equations

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

def CircuitComplexity.AONForM {N M : ℕ} [NeZero N] [NeZero M] (f : BitString N → BitString M) : Circuit Basis.unboundedAON 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 CircuitComplexity.AONForM_is_Correct {N M : ℕ} [NeZero N] [NeZero M] (f : BitString N → BitString M) : (AONForM f).eval = f

The multi-output DNF circuit correctly computes f.

instance CircuitComplexity.instCompleteBasisUnboundedAON : CompleteBasis Basis.unboundedAON