Documentation

Complexitylib.Circuits.KeyedMinimumTournament

Keyed minimum tournaments #

This module exposes a sequential circuit tournament that selects one minimum-key record from any nonempty fixed-width family while retaining its payload.

source
theorem Complexity.BitString.keyedTournamentInputWidth_eq (count recordWidth : ℕ) :
keyedTournamentInputWidth count recordWidth = (count + 1) * recordWidth

The recursive record layout is the usual row count times record width.

source
theorem Complexity.BitString.exists_unsignedMinimumKeyedRecord_eq {keyWidth payloadWidth : ℕ} (count : ℕ) (keys : Fin (count + 1) → BitString keyWidth) (payloads : Fin (count + 1) → BitString payloadWidth) :
∃ (index : Fin (count + 1)), unsignedMinimumKeyedRecord count keys payloads = (keys index, payloads index)

The tournament winner is one of the supplied key-payload records.

source
theorem Complexity.BitString.unsignedMinimumKeyedRecord_key_le {keyWidth payloadWidth : ℕ} (count : ℕ) (keys : Fin (count + 1) → BitString keyWidth) (payloads : Fin (count + 1) → BitString payloadWidth) (index : Fin (count + 1)) :
(unsignedMinimumKeyedRecord count keys payloads).1.unsignedValue ≤ (keys index).unsignedValue

The winning key is no larger than every supplied key.

source
@[simp]
theorem Complexity.Circuit.eval_unsignedKeyedMinTournament (keyWidth payloadWidth : ℕ) [NeZero keyWidth] (count : ℕ) (keys : Fin (count + 1) → BitString keyWidth) (payloads : Fin (count + 1) → BitString payloadWidth) :
(unsignedKeyedMinTournament keyWidth payloadWidth count).snd.eval (BitString.packKeyedRecords count keys payloads) = have winner := BitString.unsignedMinimumKeyedRecord count keys payloads; Fin.append winner.1 winner.2

The tournament returns the semantic left-associated minimum record.

source
@[simp]
theorem Complexity.Circuit.size_unsignedKeyedMinTournament (keyWidth payloadWidth : ℕ) [NeZero keyWidth] (count : ℕ) :
(unsignedKeyedMinTournament keyWidth payloadWidth count).snd.size = (count + 1) * (keyWidth + payloadWidth) + count * (20 * keyWidth + 5 * payloadWidth + 1)

Exact tournament size: record copies plus one keyed selector per comparison.