Parallel keyed-record circuit families -- definitions

A nonempty family of circuits with one fixed key-payload output width is packed recursively in the exact layout consumed by unsignedKeyedMinTournament.

noncomputable def Complexity.Circuit.parallelKeyedRecordFamily {B : Basis} {inputWidth keyWidth payloadWidth : ℕ} [NeZero inputWidth] [NeZero keyWidth] (count : ℕ) : (Fin (count + 1) → (internalGates : ℕ) × Circuit B inputWidth (keyWidth + payloadWidth) internalGates) → (internalGates : ℕ) × Circuit B inputWidth (BitString.keyedTournamentInputWidth count (keyWidth + payloadWidth)) internalGates

Pack count + 1 fixed-width record circuits in parallel.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.Circuit.parallelKeyedRecordFamily 0 circuits = circuits 0