Correctness of Batcher sorting networks

The ordered network sorts every finite input. The keyed network moves whole records, sorts their projected keys, and preserves the record multiset.

theorem Algebraic.MassProduction.Sorting.Semantics.orderedBitonicSort_sorted {α : Type u_1} [LinearOrder α] (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords depth) → α) : SequenceSorted ascending (orderedBitonicSort depth ascending input)

Batcher's ordered network sorts every input sequence.

theorem Algebraic.MassProduction.Sorting.Semantics.keyedBitonicSort_sorted {κ : Type u_1} {α : Sort u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords depth) → α) : SequenceSorted ascending fun (output : Fin (networkRecords depth)) => key (keyedBitonicSort key depth ascending input output)

The keyed network sorts records by their projected keys.

theorem Algebraic.MassProduction.Sorting.Semantics.keyedBitonicSort_permutes {κ : Type u_1} {α : Type u_2} [LinearOrder κ] (key : α → κ) (depth : ℕ) (ascending : Bool) (input : Fin (networkRecords depth) → α) : SequencePermutes (keyedBitonicSort key depth ascending input) input

The keyed network preserves complete records up to permutation.