feat(algorithms): add stable bubble sort

[Robertboy18]

This PR adds the stable bubble sort! The algorithm works in the usual way: each pass bubbles one maximal element to the end, then recursively sorts the remaining prefix. The stability proof follows the implementation pretty directly. We only swap when the next element is strictly smaller, so equal elements are never exchanged and keep their original order.

The PR proves that bubbleSort returns a sorted permutation of the input, preserves equal-value order via StableByValue, and runs within a quadratic comparison bound.

Validation:

• lake build Cslib

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Adds a stable bubble sort implementation for Lean lists (with comparison-counting in TimeM) and a shared stability predicate used to state/prove stability.

Changes:

• Introduces StableByValue as a reusable stability predicate for list sorts.
• Adds bubbleSort (stable) returning TimeM ℕ (List α), plus correctness + time complexity theorems.
• Exposes the new modules via Cslib.lean imports.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.

File	Description
Cslib/Algorithms/Lean/Sorting.lean	Adds a stability predicate (StableByValue) intended for stable-sort proofs.
Cslib/Algorithms/Lean/BubbleSort/BubbleSort.lean	Implements stable bubble sort in TimeM with proofs (perm/stable/sorted) and a cost bound.
Cslib.lean	Re-exports the new sorting utilities and bubble sort module at the library root.