feat: prove Array.qsort correct

[kim-em]

This PR adds library theorems establishing that Array.qsort preserves its input and returns an ordered result.

The proofs are designed for the three-way implementation introduced in #14653. They establish preservation of size, permutation and membership, preservation of elements outside the requested interval, orderedness of arbitrary sorted slices, orderedness of complete results, and adjacent-element variants. The theorems live in Init.Data.Array.QSort.Lemmas and are publicly re-exported by Init.Data.Array.QSort.

This replaces the implementation-coupled, grind-based test-suite verification from #7995. It incorporates the goals of the later completion attempt #12510 and follows the earlier replacement-sort proof work in #5346. The Zulip verification discussion provides additional context for moving these results into the library alongside the new implementation.

🤖 prepared with assistance from codex and claude

[cursor]

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e51752cf2f9a8b305e67ea90c5aa631b210056ce --onto 5b8d06c1764fa367a1e27b3e89f64667eac425af. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-02 09:50:57)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e51752cf2f9a8b305e67ea90c5aa631b210056ce --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-02 09:50:58)