Constant and primary-input source circuits

This module exposes zero-internal-gate circuits whose outputs independently choose a constant or copy one primary input.

@[simp]

theorem Complexity.Circuit.eval_inputSources {inputWidth outputWidth : ℕ} [NeZero inputWidth] [NeZero outputWidth] (sources : Fin outputWidth → InputSource inputWidth) (input : BitString inputWidth) : (inputSources sources).eval input = fun (output : Fin outputWidth) => (sources output).eval input

Source tuples evaluate pointwise to their specified constants or inputs.

@[simp]

theorem Complexity.Circuit.size_inputSources {inputWidth outputWidth : ℕ} [NeZero inputWidth] [NeZero outputWidth] (sources : Fin outputWidth → InputSource inputWidth) : (inputSources sources).size = outputWidth

An outputWidth-source tuple has exactly that many counted output gates.