-- The unit sphere is paradoxical under the rotation group, from
-- Hausdorff's paradox and the absorption of the countable fixed set
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Geometry.Sphere.Paradox
import Absorb
import Geometry.Hausdorff.Paradox
import Algebra.Group.Paradox.Transfer

theorem sphere.paradoxical
  shows Paradoxical(sphereAction, SO3, S²)
proof
  have action := sphereAction.action
  have subset := difference.subset_left at S², wordFixedSet
  have whole := sphere.absorb_any
    with wordFixedSet.countable, wordFixedSet.subset
  exact Paradoxical.of_equidecomposable
    with action, subset, whole, hausdorff.pieces