Formalize $BB(5)=47\,176\,870$ in Lean 4 (the 5-state, 2-symbol busy beaver value)

Prove in Lean 4 the theorem (currently a `sorry` in google-deepmind/formal-conjectures): ``` theorem BB_5 : BB 5 = 47176870 ``` where `BB n := sSup { N | ∃ C : Candidate n, C.M.haltingNumber = N }` is the maximum halting time (max-shift function) over all $n$-state, $2$-symbol Turing machines started on a blank tape (the repo's `Candidate n` bundles such a halting machine). Meaning: the 5-state busy-beaver (maximum-shifts) number is exactly $47176870$.

Acceptance. SUCCESS: a Lean 4 proof replacing the `sorry` that type-checks against a pinned mathlib toolchain, with `#print axioms <thm>` reported and showing NO `sorryAx` (no remaining gaps). Both the $\ge$ (exhibit the champion) and $\le$ (all others) sides of the `sSup` must be established. DISCLOSURE: this is an enormous computational certificate — a `native_decide`/reflection-heavy proof almost certainly enlarges the TCB (`Lean.ofReduceBool`, `Lean.trustCompiler`) and MUST be disclosed; a pure-kernel proof would be a landmark. PARTIAL credit: formalizing `BB_1..BB_4` (values $1,6,21,107$), or the lower bound `47176870 ≤ BB 5` alone via the known champion machine.