feat(Algorithms): add BubbleSort formalization with correctness and time bounds

[patternscientist]

This PR adds a Lean formalization of BubbleSort in TimeM ℕ (List α).

Included:

• bubble, bubbleSortAux, and bubbleSort
• a functional correctness proof showing that bubbleSort returns a sorted permutation of the input
• a time bound showing that the number of comparisons is at most n.choose 2

The development follows the standard BubbleSort invariant that one left-to-right sweep moves a maximum element to the end.

For context, there is another open PR that includes BubbleSort as part of a broader algorithm bundle (leanprover/cslib#383); this PR is a focused TimeM-based BubbleSort formalization in current CSLib style, with explicit functional correctness and comparison-count bounds.

Checks run locally:

• lake build
• lake test
• lake exe checkInitImports
• lake exe mk_all --module