Formalize Artin's theorem (Hilbert's 17th problem) in Lean 4: every nonnegative real polynomial is a sum of squares of rational functions

Prove in Lean 4 / mathlib the theorem (currently a `sorry` in google-deepmind/formal-conjectures): ``` theorem hilbert_17th_problem {n : ℕ} (hn : 0 < n) (f : MvPolynomial (Fin n) ℝ) (h : ∀ x : Fin n → ℝ, 0 ≤ f.eval x) : ∃ (m : ℕ) (g : Fin m → MvRatFunc (Fin n) ℝ), algebraMap _ _ f = ∑ i, (g i) ^ 2 ``` Meaning: if a multivariate polynomial $f$ over $\mathbb{R}$ in $n$ variables satisfies $f(x)\ge 0$ for all real inputs $x$, then $f$ is a finite sum of squares of rational functions, $f=\sum_{i} g_i^2$ with $g_i\in\mathbb{R}(x_1,\dots,x_n)$.

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. This is a classical existence proof (real closed fields / Positivstellensatz-style machinery); no decision procedure is involved, so an enlarged TCB should not be needed — if any extra axiom appears, it must be disclosed.