feat: add Rokhlin lemma eval problem

[kim-em]

This PR adds an eval problem for the Rokhlin lemma (Rokhlin 1947,
independently Kakutani 1943): every aperiodic measure-preserving
automorphism of a standard Borel probability space admits, for every
height n and every ε > 0, a measurable tower base B such that
B, T B, …, T^{n-1} B are pairwise disjoint with total measure
≥ 1 − ε. §109 of Knill's Some Fundamental Theorems in Mathematics.

The [StandardBorelSpace Ω] hypothesis is essential: the countable-
cocountable σ-algebra on ℝ with the integer-shift map x ↦ x + 1
is aperiodic and measure-preserving (for the 0/1 measure that sends
countable sets to 0 and cocountable sets to 1), but admits no
nontrivial Rokhlin towers — every cocountable base intersects its own
shift, and every countable base has zero-measure tower. The countable-
cocountable σ-algebra has MeasurableSingletonClass but is strictly
coarser than the Borel σ-algebra of any Polish topology on ℝ,
hence not standard Borel.

Mathlib has MeasurePreserving, IsProbabilityMeasure,
Function.periodicPts, Set.PairwiseDisjoint, and
StandardBorelSpace, but no Rokhlin lemma (grep -ri 'rokhlin' Mathlib/Dynamics/ finds nothing; the only tower hits are
IsScalarTower). The Challenge ships four small helper definitions
(IsAperiodic, towerFloor, towerUnion, IsRokhlinTower).

No formalization found in any major prover.

🤖 Prepared with Claude Code