Keyed minimum tournaments -- definitions

The tournament consumes count + 1 key-payload records. Its recursively appended input layout makes each construction step a literal prefix projection plus one final-record projection, avoiding arithmetic casts in the circuit DAG.

def Complexity.BitString.keyedTournamentInputWidth : ℕ → ℕ → ℕ

Width of count + 1 recursively appended fixed-width records.

Equations

• Complexity.BitString.keyedTournamentInputWidth 0 x✝ = x✝
• Complexity.BitString.keyedTournamentInputWidth count.succ x✝ = Complexity.BitString.keyedTournamentInputWidth count x✝ + x✝

instance Complexity.BitString.instNeZeroKeyedTournamentInputWidth (count keyWidth payloadWidth : ℕ) [NeZero keyWidth] : NeZero (keyedTournamentInputWidth count (keyWidth + payloadWidth))

def Complexity.BitString.packKeyedRecords {keyWidth payloadWidth : ℕ} (count : ℕ) : (Fin (count + 1) → BitString keyWidth) → (Fin (count + 1) → BitString payloadWidth) → BitString (keyedTournamentInputWidth count (keyWidth + payloadWidth))

Pack count + 1 key-payload records by recursively appending the last one.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.BitString.packKeyedRecords 0 keys payloads = Fin.append (keys 0) (payloads 0)

def Complexity.BitString.unsignedMinimumKeyedRecord {keyWidth payloadWidth : ℕ} (count : ℕ) : (Fin (count + 1) → BitString keyWidth) → (Fin (count + 1) → BitString payloadWidth) → BitString keyWidth × BitString payloadWidth

Semantic winner of a left-associated keyed minimum tournament.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.BitString.unsignedMinimumKeyedRecord 0 keys payloads = (keys 0, payloads 0)

noncomputable def Complexity.Circuit.unsignedKeyedMinTournament (keyWidth payloadWidth : ℕ) [NeZero keyWidth] (count : ℕ) : (internalGates : ℕ) × Circuit Basis.andOr2 (BitString.keyedTournamentInputWidth count (keyWidth + payloadWidth)) (keyWidth + payloadWidth) internalGates

Sequential keyed-minimum tournament over count + 1 packed records.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.Circuit.unsignedKeyedMinTournament keyWidth payloadWidth 0 = ⟨0, Complexity.Circuit.projectInputs fun (input : Fin (keyWidth + payloadWidth)) => input⟩