Formalize Shitov's cubic upper bound for synchronizing words (best known bound toward the Cerný conjecture)

Prove in Lean 4 the theorem (currently a `sorry` in google-deepmind/formal-conjectures): ``` theorem shitov_upper_bound : ∃ f : ℝ → ℝ, f =o[atTop] (fun n : ℝ => n ^ 3) ∧ ∀ {α σ : Type*} [Fintype σ] (M : DFA α σ) (hM : M.IsSynchronizing), ∃ w : List α, M.IsSynchronizingWord w ∧ (w.length : ℝ) ≤ (7 / 48 + 2 * 15625 / 1597536) * (Fintype.card σ : ℝ) ^ 3 + f (Fintype.card σ : ℝ) ``` Meaning: every synchronizing DFA on $n$ states has a reset (synchronizing) word of length at most $\left(\tfrac{7}{48}+\tfrac{2\cdot 15625}{1597536}\right)n^3+o(n^3)\approx 0.1654\,n^3$.

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). Expected pure-kernel: the only axioms should be `[propext, Classical.choice, Quot.sound]`; state explicitly that this holds. The statement is analytic (`Asymptotics.IsLittleO` over $\mathbb{R}$) with a combinatorial core, so a pure-kernel proof is expected; any reflection/decision axiom must be disclosed.