AND/OR/NOT Basis

This module provides the AND/OR basis definitions and completeness results.

Definitions (from Complexitylib.Circuits.AndOrNot.Defs)

• AndOrOp — AND/OR operations
• Basis.unboundedAndOr — unbounded fan-in AND/OR basis
• Basis.boundedAndOr k — fan-in ≤ k AND/OR basis
• Basis.andOr2 — fan-in exactly 2 AND/OR basis

Main results

• CompleteBasis Basis.unboundedAndOr — proved via DNF construction
• CompleteBasis Basis.andOr2 — proved via gate-chain simulation from unboundedAndOr, using CompleteBasis.of_simulation
• CompileAndOr.compileFn_eval — exact semantics of that simulation
• CompileAndOr.compileFn_size_le — its quantitative size overhead

@[simp]

theorem Complexity.CompileAndOr.compileFn_eval {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr N M G) : (compileFn c).eval = c.eval

Compiling unbounded fan-in AND/OR gates to fan-in two preserves the circuit's complete multi-output semantics.

@[simp]

theorem Complexity.CompileAndOr.compileFn_size {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr N M G) : (compileFn c).size = G' c + M

The compiled circuit has one public output gate for each source output, in addition to the internal gate chains.

theorem Complexity.CompileAndOr.compileFn_size_le {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit Basis.unboundedAndOr N M G) : (compileFn c).size ≤ c.totalFanIn + c.size + M

Gate-chain simulation has size at most source total fan-in plus source size plus one passthrough gate per output.