The full binary basis

Every gate of the full binary basis B₂ computes one of the sixteen Boolean functions of two bits. Both argument slots may read the same wire, fan-out is unrestricted, and every gate costs one. This is the basis of the (4 - ε) n circuit lower bound in Algebraic.LowerBound.Cutwidth.

@[reducible, inline]

abbrev Algebraic.Binary.Op : Type

An operation symbol of the full binary basis is a Boolean function of two bits.

Equations

• Algebraic.Binary.Op = (Bool → Bool → Bool)

theorem Algebraic.Binary.card_op : Fintype.card Op = 16

The sixteen binary Boolean functions.

@[reducible, inline]

abbrev Algebraic.Binary.signature : Signature

The signature of the full binary basis: every symbol takes two arguments.

Equations

• Algebraic.Binary.signature = { Op := Algebraic.Binary.Op, Arity := fun (x : Algebraic.Binary.Op) => 2 }

def Algebraic.Binary.interpretation : Interpretation signature Bool

The Boolean interpretation applies the symbol to its two argument bits.

Equations

• Algebraic.Binary.interpretation op arguments = op (arguments 0) (arguments 1)

@[simp]

theorem Algebraic.Binary.interpretation_apply (op : Op) (arguments : Fin 2 → Bool) : interpretation op arguments = op (arguments 0) (arguments 1)

theorem Algebraic.Binary.program_fanInAtMost_two {n g : ℕ} (program : Program signature n g) : program.FanInAtMost 2

Every gate of a binary program has fan-in two.

theorem Algebraic.Binary.circuit_fanInAtMost_two {n m : ℕ} (circuit : Circuit signature n m) : circuit.FanInAtMost 2

Every gate of a binary circuit has fan-in two.