Formalize Hilbert's 1888 characterization of when nonnegative forms are sums of squares of polynomials

With `Hilbert17thProblemHomogenousPoly n d` := every homogeneous degree-$2d$ form in $n$ real variables that is everywhere $\ge 0$ is a sum of squares of polynomials, prove (currently a `sorry`): ``` theorem hilbert_17th_problem_poly {n d : ℕ} (hn : 0 < n) (hd : 0 < d) : Hilbert17thProblemHomogenousPoly n d ↔ n = 1 ∨ n = 2 ∨ d = 1 ∨ n = 3 ∧ d = 2 ``` Meaning: nonnegative real forms of degree $2d$ in $n$ variables are ALL sums of squares of polynomials if and only if $n=1$, or $n=2$, or $d=1$, or $(n,d)=(3,2)$.

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 `←` direction needs explicit SOS representations in the four listed regimes; the `→` direction needs counterexamples (e.g. Motzkin) in the remaining regimes. PARTIAL: either implication, or the `f_not_sum_of_squares` lemma (Motzkin not SOS-of-polynomials), itself a `sorry` in the same file.