The zero-one argument for bitonic splitting

Thresholding a tuple at any pivot preserves its four-point bitonic invariant. A finite kernel-checked Boolean lemma therefore proves that pairwise minima and maxima of two halves remain bitonic over every linear order.

Main results

• Cslib.BitonicSort.IsBitonic.min_halves: pairwise minima preserve the invariant.
• Cslib.BitonicSort.IsBitonic.max_halves: pairwise maxima preserve the invariant.

References

• Adapted from MassProduction/SortingSemantics/Boolean.lean and the threshold argument in SortingSemantics/Internal.lean in S. Schlesinger, Boolean circuit mass production formalization.

theorem Cslib.BitonicSort.IsBitonic.min_halves {α : Type u_1} [LinearOrder α] {n : ℕ} (first second : Fin n → α) (hsequence : IsBitonic (Fin.append first second)) : IsBitonic (first ⊓ second)

The minima of corresponding entries in the two halves of a bitonic tuple are bitonic.

theorem Cslib.BitonicSort.IsBitonic.dual {α : Type u_1} [LinearOrder α] {n : ℕ} {input : Fin n → α} (h : IsBitonic input) : IsBitonic input

Reversing the value order exchanges the two four-point inequalities.

theorem Cslib.BitonicSort.IsBitonic.max_halves {α : Type u_1} [LinearOrder α] {n : ℕ} (first second : Fin n → α) (h : IsBitonic (Fin.append first second)) : IsBitonic (first ⊔ second)

The maxima of corresponding entries in the two halves of a bitonic tuple are bitonic.