feat: add Ornstein–Weiss ℤᵈ Rokhlin lemma eval problem

[kim-em]

This PR adds an eval problem for the Ornstein–Weiss ℤᵈ Rokhlin
lemma (Ornstein–Weiss, 1987): the multidimensional generalization of
the classical Rokhlin lemma. For every free measure-preserving
ℤᵈ-action T on a standard Borel probability space (with d ≥ 1,
identity axiom T 0 = id, and the homomorphism axiom), every box size
N ≥ 1, and every ε > 0, there is a measurable base B such that
the translates T v '' B for v ∈ [0, N)ᵈ are pairwise disjoint
with measure ≥ 1 − ε. Additional statement of §109 of Knill's
Some Fundamental Theorems in Mathematics (the boxed main theorem
is the classical Rokhlin lemma).

Mathlib has MeasurePreserving, IsProbabilityMeasure,
Set.PairwiseDisjoint, Fintype.piFinset, Finset.Ico, and
StandardBorelSpace, but no Ornstein–Weiss lemma, no free
measure-preserving ℤᵈ-actions, no multidimensional Rokhlin towers.
The Challenge ships two small helper definitions (IsFreeAction and
boxShape).

No formalization found in any major prover.

🤖 Prepared with Claude Code