Primary-input projection circuits

This module exposes zero-internal-gate circuits that copy, permute, or duplicate primary inputs into an arbitrary positive output tuple.

@[simp]

theorem Complexity.Circuit.eval_projectInputs {N M : ℕ} [NeZero N] [NeZero M] (mapInput : Fin M → Fin N) (input : BitString N) : (projectInputs mapInput).eval input = input ∘ mapInput

Input projection evaluates by precomposing the input with the projection map.

@[simp]

theorem Complexity.Circuit.size_projectInputs {N M : ℕ} [NeZero N] [NeZero M] (mapInput : Fin M → Fin N) : (projectInputs mapInput).size = M

An M-output input projection has exactly M counted output gates.