Self-delimiting input-pair circuits

This module exposes a zero-internal-gate circuit for the canonical pairing codec used by serialized machines and circuit evaluators.

theorem Complexity.Circuit.eval_pairInputSources {inputWidth leftWidth rightWidth : ℕ} [NeZero inputWidth] (left : Fin leftWidth → InputSource inputWidth) (right : Fin rightWidth → InputSource inputWidth) (input : BitString inputWidth) : ((pairInputSources left right).eval input).toList = pair (BitString.toList fun (i : Fin leftWidth) => (left i).eval input) (BitString.toList fun (i : Fin rightWidth) => (right i).eval input)

Pair-source circuits serialize exactly the semantic values of their left and right source tuples.

@[simp]

theorem Complexity.Circuit.size_pairInputSources {inputWidth leftWidth rightWidth : ℕ} [NeZero inputWidth] (left : Fin leftWidth → InputSource inputWidth) (right : Fin rightWidth → InputSource inputWidth) : (pairInputSources left right).size = pairSourceWidth leftWidth rightWidth

Pair-source circuits pay exactly one counted output gate per serialized query bit.