feat: add Smale conjecture eval problem

[kim-em]

Summary

• Adds the Smale conjecture (Hatcher 1983) as a new eval problem in the relative parameterized form: smooth families of self-diffeomorphisms of S³ on a compact manifold-with-boundary X, whose boundary restriction already factors through O(4), deform rel ∂X to families fully factoring through O(4).
• This relative form captures π_k(Diff(S³), O(4)) = 0 for all k, which is equivalent (modulo smoothing theory) to the homotopy equivalence O(4) ≃ Diff(S³). The non-relative version would only give surjectivity on π_*.
• The Cerf case (X = point, ∂X = ∅) is the unparameterized theorem from feat: add Cerf's theorem Γ₄ = 0 eval problem #17.
• Uses (𝓡∂ n).boundary X from mathlib's InteriorBoundary API to express the boundary condition, with [NeZero n] required by mathlib for this to elaborate.

🤖 Prepared with Claude Code