-- Absorbing a countable set into the sphere: for a countable D ⊆ S² off
-- the z-axis there is a rotation ρ ∈ SO3 with ρⁿ(D) ∩ D = ∅ for every
-- n ≥ 1, and S² and S² ∖ D are SO3-equidecomposable
-- 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.Absorption.Final
import Sphere
import Pieces

-- A rotation separating D from its positive powers.
theorem sphere.exists_separating (D : Set)
  requires countable : Countable(D)
  requires subset : D ⊆ S²
  requires offAxis : ∀ d ∈ D, vectorPoint(d) ≠ complexZero
  shows ∃ ρ ∈ Group.carrier(SO3), ∀ n ∈ ℕ,
    Disjoint(actImage(sphereAction, groupPow(SO3, ρ, n + 1), D), D)
proof
  obtain ⟨t, real, separated⟩ := turn.separates with countable, subset, offAxis
  have typed : Real(t) by typecheck
  have rotation := turn.so3 at t
  exact ⟨turn(t), rotation, separated⟩

-- The sphere absorbs every countable set off the z-axis.
theorem sphere.absorb_countable (D : Set)
  requires countable : Countable(D)
  requires subset : D ⊆ S²
  requires offAxis : ∀ d ∈ D, vectorPoint(d) ≠ complexZero
  shows Equidecomposable(sphereAction, SO3, S², S², S² ∖ D)
proof
  obtain ⟨ρ, rotation, separated⟩ := sphere.exists_separating with countable, subset, offAxis
  exact sphere.absorb with rotation, subset, separated