feat: remove partial keyword and runtime bounds checks from Array.binSearch

[kim-em]

This PR completes the TODO in Init.Data.Array.BinSearch, removing the partial keyword and converting runtime bounds checks to compile time bounds checks.

[kim-em]

!bench

[leanprover-bot]

Here are the benchmark results for commit bcc22fd.
There were significant changes against commit bf13b24:

  Benchmark     Metric          Change
  ==============================================
+ simp_arith1   branch-misses    -3.2% (-24.3 σ)
- stdlib        type checking     3.1%  (11.2 σ)

[kim-em]

Seems like nothing of significance in !bench.

Once more to make sure:

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bf13b24692ce5b96cb8a9fd4a3d11c0e170dbccf --onto ba3f2b3ecf8967410f3498e2835b883601f03967. (2024-11-24 05:57:10)