Comparison Sorting Lower Bound

IsSort.lowerBound_infinite: any correct comparison sort on an infinite type has query complexity at least ⌈log₂(n!)⌉ for every input size n.

The proof constructs n! distinct total orders on α (one per permutation of n embedded elements), shows they produce distinct sorted outputs, and applies FreeM.exists_countQueries_ge_clog with LEQuery.cardResponse_le_two witnessing that all responses come from Bool (cardinality 2).

PrefixPermOrder: constructing n! distinct total orders

Main theorem

theorem Cslib.Query.IsSort.lowerBound_infinite {α : Type} [Infinite α] {sort : List α → FreeM (LEQuery α) (List α)} (hs : IsSort sort) : LowerBound sort List.length fun (n : ℕ) => Nat.clog 2 n.factorial

Any correct comparison sort on an infinite type has query complexity at least ⌈log₂(n!)⌉ for every input size n.