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.

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.AONForM_j {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

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

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

Indicator coordinate encoded by a gate index in the multi-output DNF circuit.

Equations

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

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

Gate selected by an encoded output and indicator pair in the multi-output DNF circuit.

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.