Fixed-width multiplexers

This module exposes a fan-in-two circuit selecting one of two fixed-width payloads. The control bit chooses the left payload when true and the right payload when false. The construction has exactly three gates per payload bit.

theorem Complexity.Circuit.eval_multiplexer_packed (width : ℕ) [NeZero width] (input : BitString (1 + (width + width))) (coordinate : Fin width) : (multiplexer width).eval input coordinate = if input ⟨0, ⋯⟩ = true then input ⟨1 + ↑coordinate, ⋯⟩ else input ⟨1 + width + ↑coordinate, ⋯⟩

Pointwise semantics on the multiplexer circuit's packed input.

@[simp]

theorem Complexity.Circuit.eval_multiplexer (width : ℕ) [NeZero width] (control : Bool) (left right : BitString width) : (multiplexer width).eval (BitString.multiplexerInput control left right) = if control = true then left else right

The multiplexer selects the left payload exactly when its control is true.

@[simp]

theorem Complexity.Circuit.size_multiplexer (width : ℕ) [NeZero width] : (multiplexer width).size = 3 * width

A width-bit multiplexer has exactly three gates per payload bit.