-- The absorption theorem as an equidecomposability: for act : G ↷ X,
-- D ⊆ X, and ρ ∈ G with ρⁿ⁺¹(D) ∩ D = ∅ for every n, the sets X and X ∖ D
-- are equidecomposable under the action with the two pieces U = ⋃ₙ ρⁿ(D),
-- carried by ρ, and X ∖ U, carried by the unit; in particular the unit
-- sphere S² and S² ∖ D are equidecomposable under the rotation group SO3
-- 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.Pieces
import Absorb
import Algebra.Group.Paradox
import Rotation.Orthogonal

section Pieces
variable (act G X : Set)
hypothesis action : act : G ↷ X

-- The image of a subset of X under g, in the two spellings.
theorem actImage.eq_translate (g : G) (A : Set)
  requires subset : A ⊆ X
  shows translate(act, X, g, A) = actImage(act, g, A)
proof
  ext y
  constructor
  . intro hy
    have data := translate.membership.forward with hy
    obtain ⟨inX, x, hx, shape⟩ := data
    apply actImage.membership.backward
    refine ⟨x, hx, ?_⟩
    symm
    exact shape
  . intro hy
    obtain ⟨x, hx, shape⟩ := actImage.membership.forward with hy
    have xIn := subset with x, hx
    have moved : g ·ₐ x ∈ X := Action.act_mem with action, xIn
    rw shape at moved
    symm at shape
    apply translate.membership.backward
    exact ⟨moved, x, hx, shape⟩

theorem translate.unit (A : Set)
  requires subset : A ⊆ X
  shows translate(act, X, G.one, A) = A
proof
  have group := Action.group with action
  ext y
  constructor
  . intro hy
    obtain ⟨inX, x, hx, shape⟩ := translate.membership.forward with hy
    have fixed : G.one ·ₐ x = x := one_act with action, (subset with x, hx)
    rw [shape, fixed]
    exact hx
  . intro hy
    have yIn := subset with y, hy
    have fixed : G.one ·ₐ y = y := one_act with action, yIn
    apply translate.membership.backward
    refine ⟨yIn, y, hy, ?_⟩
    rw fixed
    rfl

-- The absorption theorem: X and X ∖ D are equidecomposable.
theorem absorption.equidecomposable (ρ : G) (D : Set)
  requires subset : D ⊆ X
  requires separated : ∀ n ∈ ℕ, Disjoint(actImage(act, ρ ^ (n + 1), D), D)
  shows Equidecomposable(act, G, X, X, X ∖ D)
proof
  have group := Action.group with action
  have unitIn : G.one ∈ G := Group.one_mem with group
  have rhoIn : ρ ∈ G by assumption
  have orbitSubset : forwardOrbit(act, G, ρ, D) ⊆ X := forwardOrbit.subset with *
  have orbitContains : D ⊆ forwardOrbit(act, G, ρ, D) := forwardOrbit.contains with *
  have carried := forwardOrbit.image with action, subset, separated
  have restSubset := difference.subset_left at X, forwardOrbit(act, G, ρ, D)
  have disjoint := Disjoint.difference_right at X, forwardOrbit(act, G, ρ, D)
  have cover := difference.union2_of_subset with orbitSubset
  have movedOrbit : translate(act, X, ρ, forwardOrbit(act, G, ρ, D)) = actImage(act, ρ, forwardOrbit(act, G, ρ, D)) :=
    actImage.eq_translate with *
  have movedRest : translate(act, X, G.one, X ∖ forwardOrbit(act, G, ρ, D)) = X ∖ forwardOrbit(act, G, ρ, D) :=
    translate.unit with *
  have disjointImages : Disjoint(translate(act, X, ρ, forwardOrbit(act, G, ρ, D)),
      translate(act, X, G.one, X ∖ forwardOrbit(act, G, ρ, D)))
    rw [movedOrbit, movedRest, carried]
    apply Disjoint.iff.backward
    intros y hy hy2
    obtain ⟨inOrbit, notInD⟩ := difference.membership.forward with hy
    obtain ⟨inX, notInOrbit⟩ := difference.membership.forward with hy2
    exact notInOrbit with inOrbit
  have coverImages : translate(act, X, ρ, forwardOrbit(act, G, ρ, D)) ∪ translate(act, X, G.one, X ∖ forwardOrbit(act, G, ρ, D)) = X ∖ D
    rw [movedOrbit, movedRest, carried]
    ext y
    constructor
    . intro hy
      have sides := union2.membership.forward with hy
      cases sides with inLeft | inRight
      . obtain ⟨inOrbit, notInD⟩ := difference.membership.forward with inLeft
        have inX := orbitSubset with y, inOrbit
        exact difference.membership.backward with ⟨inX, notInD⟩
      . obtain ⟨inX, notInOrbit⟩ := difference.membership.forward with inRight
        have notInD : ¬(y ∈ D)
          intro inD
          exact notInOrbit with (orbitContains with y, inD)
        exact difference.membership.backward with ⟨inX, notInD⟩
    . intro hy
      obtain ⟨inX, notInD⟩ := difference.membership.forward with hy
      have alternatives : y ∈ forwardOrbit(act, G, ρ, D) ∨ ¬(y ∈ forwardOrbit(act, G, ρ, D)) by tauto
      apply union2.membership.backward
      cases alternatives with inOrbit | notInOrbit
      . left
        exact difference.membership.backward with ⟨inOrbit, notInD⟩
      . right
        exact difference.membership.backward with ⟨inX, notInOrbit⟩
  exact Equidecomposable.of_two_pieces at act, G, X, X, X ∖ D,
    forwardOrbit(act, G, ρ, D), X ∖ forwardOrbit(act, G, ρ, D), ρ, G.one with
    action, rhoIn, unitIn, orbitSubset, restSubset, disjoint, cover,
    disjointImages, coverImages

end Pieces

-- Absorbing a set into the sphere: for D ⊆ S² and a rotation ρ with
-- ρⁿ⁺¹(D) ∩ D = ∅ for every n, S² and S² ∖ D are SO3-equidecomposable.
theorem sphere.absorb (ρ D : Set)
  requires rotation : ρ ∈ Group.carrier(SO3)
  requires subset : D ⊆ S²
  requires separated : ∀ n ∈ ℕ,
    Disjoint(actImage(sphereAction, groupPow(SO3, ρ, n + 1), D), D)
  shows Equidecomposable(sphereAction, SO3, S², S², S² ∖ D)
proof
  have action := sphereAction.action
  exact absorption.equidecomposable with action, rotation, subset, separated