Keyed minimum tournaments -- proof internals

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

theorem Complexity.BitString.exists_unsignedMinimumKeyedRecord_eq_internal {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)

theorem Complexity.BitString.unsignedMinimumKeyedRecord_key_le_internal {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

theorem Complexity.Circuit.eval_unsignedKeyedMinTournament_internal (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

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