Parallel keyed-record circuit families

This module packs a nonempty fixed-width family of key-payload circuits into the recursive record layout consumed by the verified minimum tournament.

theorem Complexity.Circuit.eval_parallelKeyedRecordFamily {B : Basis} {inputWidth keyWidth payloadWidth : ℕ} [NeZero inputWidth] [NeZero keyWidth] (count : ℕ) (circuits : Fin (count + 1) → (internalGates : ℕ) × Circuit B inputWidth (keyWidth + payloadWidth) internalGates) (input : BitString inputWidth) (keys : Fin (count + 1) → BitString keyWidth) (payloads : Fin (count + 1) → BitString payloadWidth) (heval : ∀ (index : Fin (count + 1)), (circuits index).snd.eval input = Fin.append (keys index) (payloads index)) : (parallelKeyedRecordFamily count circuits).snd.eval input = BitString.packKeyedRecords count keys payloads

Packed family evaluation recursively appends every key-payload record.

@[simp]

theorem Complexity.Circuit.size_parallelKeyedRecordFamily {B : Basis} {inputWidth keyWidth payloadWidth : ℕ} [NeZero inputWidth] [NeZero keyWidth] (count : ℕ) (circuits : Fin (count + 1) → (internalGates : ℕ) × Circuit B inputWidth (keyWidth + payloadWidth) internalGates) : (parallelKeyedRecordFamily count circuits).snd.size = ∑ index : Fin (count + 1), (circuits index).snd.size

Packed family size is exactly the sum of the source circuit sizes.