feat: add Schoenflies theorem eval problem

[kim-em]

This PR adds an eval problem for the Schoenflies theorem (strong form):
for every Jordan curve in the plane there is a self-homeomorphism of
ℝ² carrying the curve to the standard unit circle. §48 of Knill's
Some Fundamental Theorems in Mathematics.

The strong form is the faithful encoding of Knill's prose statement
that "each complementary region is homeomorphic to the open disk" —
the literal version is false for the unbounded region (homeomorphic to
ℝ² ∖ closedBall 0 1, fundamental group ℤ, vs. simply connected
disk). The strong form here implies the bounded-region claim.

Mathlib has Metric.sphere, EuclideanSpace, and Homeomorph, but
no Schoenflies theorem (grep -ri 'schoenflies' Mathlib/: no hits),
no Jordan curve theorem, no invariance-of-domain machinery in a form
that would discharge it. Stateable with zero new definitions.

No formalization found in any major prover.

🤖 Prepared with Claude Code