-- The Banach–Tarski paradox: the closed unit ball of ℝ³ is paradoxical
-- under the motions, and a part of it is equidecomposable with the
-- disjoint union of two balls; the strong form is in BanachTarski/Strong
-- 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.BanachTarski
import Sphere
import Euclid
import Algebra.Group.Paradox.Transfer

-- The punctured ball is paradoxical under the rotations: the two pieces
-- of the sphere lift to their cones.
theorem puncturedBall.pieces
  shows ∃ A, ∃ B, A ⊆ puncturedBall ∧ B ⊆ puncturedBall ∧
    Disjoint(A, B) ∧
    Equidecomposable(spaceAction, SO3, ℝ³, A, puncturedBall) ∧
    Equidecomposable(spaceAction, SO3, ℝ³, B, puncturedBall)
proof
  obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ :=
      sphere.paradoxical
  have whole := Subset.reflexive at S²
  have coneA := cone.subset_punctured with boundedA
  have coneB := cone.subset_punctured with boundedB
  have apart := cone.disjoint with boundedA, boundedB, disjoint
  have liftA := cone.equidecomposable with boundedA, whole, firstA
  have liftB := cone.equidecomposable with boundedB, whole, secondB
  rw cone.sphere at liftA
  rw cone.sphere at liftB
  witness cone(A)
  witness cone(B)
  exact ⟨coneA, coneB, apart, liftA, liftB⟩

theorem puncturedBall.paradoxical
  shows Paradoxical(restrictAction(spaceAction, SO3, puncturedBall), SO3,
      puncturedBall)
proof
  have action := spaceAction.action
  have pieces := puncturedBall.pieces
  exact Paradoxical.to_restrict with action, puncturedBall.subset_space, pieces

-- The Banach–Tarski paradox: under the motions, the rotations embed and
-- the center is absorbed, so two disjoint parts of the ball are each
-- equidecomposable with the ball.
theorem banachTarski
  shows ∃ A, ∃ B, A ⊆ unitBall ∧ B ⊆ unitBall ∧ Disjoint(A, B) ∧
    Equidecomposable(motionAction, Motions, ℝ³, A, unitBall) ∧
    Equidecomposable(motionAction, Motions, ℝ³, B, unitBall)
proof
  obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ :=
      puncturedBall.pieces
  have action := motionAction.action
  have action2 := spaceAction.action
  have hom := rotationMotion.hom
  have compatible := rotationMotion.compatible
  have liftA :=
      Equidecomposable.of_hom with action, action2, hom, compatible, firstA
  have liftB :=
      Equidecomposable.of_hom with action, action2, hom, compatible, secondB
  have center := unitBall.absorb_center
  have back := Equidecomposable.symmetric with action, center
  have wholeA := Equidecomposable.transitive with action, liftA, back
  have wholeB := Equidecomposable.transitive with action, liftB, back
  have inA := Subset.transitive with boundedA, puncturedBall.subset
  have inB := Subset.transitive with boundedB, puncturedBall.subset
  witness A
  witness B
  exact ⟨inA, inB, disjoint, wholeA, wholeB⟩

-- The same pieces, as a paradoxical decomposition of the ball under the
-- action graph restricted to the ball.
theorem banachTarski.restricted
  shows Paradoxical(restrictAction(motionAction, Motions, unitBall), Motions,
      unitBall)
proof
  have action := motionAction.action
  have pieces := banachTarski
  exact Paradoxical.to_restrict with action, unitBall.subset, pieces

-- The ball translated by (3, 0, 0), disjoint from the ball.
defgraph farPoint (i ∈ 3) : ℝ := pick3((3:R), (0:R), (0:R), i)
proof
  have three : (3:R) ∈ ℝ by typecheck
  have zero : (0:R) ∈ ℝ by typecheck
  exact pick3.real with three, zero, zero, member

instance farPoint.vector
  shows farPoint : 3 → ℝ
proof
  exact farPoint.function

theorem farPoint.zero
  shows farPoint(0) = (3:R)
proof
  have value := farPoint.value at 0 with index.zero_mem
  rw [value, pick3.zero]
  rfl

def shiftedBall : Set :=
  translate(motionAction, ℝ³, (matrixRing(realRing, 3)[1], farPoint),
    unitBall)

theorem shiftedBall.graph
  shows shiftedBall =
    translate(motionAction, ℝ³, (matrixRing(realRing, 3)[1], farPoint),
      unitBall)
proof
  simp [shiftedBall]

theorem unitBall.shift_disjoint
  shows Disjoint(unitBall, shiftedBall)
proof
  have one := Matrix.one_matrix
  have oneIn := so3Matrices.one_mem
  have far := farPoint.vector
  have farIn : farPoint ∈ ℝ³ := ℝ³.of_function with far
  apply Disjoint.iff.backward
  intros x hx hx2
  rw shiftedBall.graph at hx2
  obtain ⟨xIn, y, hy, shape⟩ := translate.membership.forward with hx2
  obtain ⟨xSpace, xBound⟩ := unitBall.membership.forward with hx
  obtain ⟨ySpace, yBound⟩ := unitBall.membership.forward with hy
  have vectorX := ℝ³.function with xSpace
  have vectorY := ℝ³.function with ySpace
  have value := motionAction.apply at matrixRing(realRing, 3)[1], farPoint,
      y with
    oneIn, farIn, ySpace
  have unitAct := matrixVector.one at y with vectorY
  rw [value, unitAct] at shape
  have e0 := addVector.entry at y, farPoint, 0 with vectorY, far, index.zero_mem
  rw farPoint.zero at e0
  have x0 : (x(0):R) = (y(0):R) + (3:R)
    rw shape
    exact e0
  have x1 := vector.component_real at x, 1 with vectorX, index.one_mem
  have x2 := vector.component_real at x, 2 with vectorX, index.two_mem
  have y0 := vector.component_real at y, 0 with vectorY, index.zero_mem
  have y1 := vector.component_real at y, 1 with vectorY, index.one_mem
  have y2 := vector.component_real at y, 2 with vectorY, index.two_mem
  have x0Real := vector.component_real at x, 0 with vectorX, index.zero_mem
  have sqX1 := realMulValue.square_nonnegative at (x(1):R)
  have sqX2 := realMulValue.square_nonnegative at (x(2):R)
  have sqY1 := realMulValue.square_nonnegative at (y(1):R)
  have sqY2 := realMulValue.square_nonnegative at (y(2):R)
  rw normSq.value at xBound
  rw normSq.value at yBound
  have sumY : (1:R) + (y(0):R) ∈ ℝ by typecheck
  have sqY := realMulValue.square_nonnegative at (1:R) + (y(0):R)
  have expandY : ((1:R) + (y(0):R)) * ((1:R) + (y(0):R)) =
      (1:R) + (2:R) * (y(0):R) + (y(0):R) * (y(0):R)
    ring
  have lowY : -(1:R) ≤ (y(0):R) by linarith
  have lowX : (2:R) ≤ (x(0):R) by linarith
  have differenceX : (x(0):R) - (2:R) ∈ ℝ by typecheck
  have sqX := realMulValue.square_nonnegative at (x(0):R) - (2:R)
  have expandX : ((x(0):R) - (2:R)) * ((x(0):R) - (2:R)) =
      (x(0):R) * (x(0):R) - (4:R) * (x(0):R) + (4:R)
    ring
  linarith

-- A part of the ball is equidecomposable with the disjoint union of the
-- ball and its translate.
theorem banachTarski.two_balls_part
  shows ∃ C, C ⊆ unitBall ∧
    Equidecomposable(motionAction, Motions, ℝ³, C, unitBall ∪ shiftedBall)
proof
  obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ :=
      banachTarski
  have action := motionAction.action
  have group := Motions.group
  have one := Matrix.one_matrix
  have oneIn := so3Matrices.one_mem
  have farIn : farPoint ∈ ℝ³ := ℝ³.of_function with farPoint.vector
  have shiftIn : (matrixRing(realRing, 3)[1], farPoint) ∈ Motions.carrier
    rw Motions.carrierOf
    exact motions.pair with oneIn, farIn
  have unitIn : Group.one(Motions) ∈ Group.carrier(Motions) := Group.one_mem
      with group
  have emptySubset : ∅ ⊆ ℝ³ := empty.subset at ℝ³
  have emptyDisjoint : Disjoint(unitBall, ∅) :=
    Disjoint.empty_right at unitBall
  have cover : unitBall ∪ ∅ = unitBall := union2.right_empty at unitBall
  have movedEmpty : translate(motionAction, ℝ³, Motions.one, ∅) = ∅
    apply Subset.antisymmetric
    . intros z hz
      obtain ⟨zIn, w, hw, equal⟩ := translate.membership.forward with hz
      exfalso
      settle with set.empty
    . exact empty.subset at translate(motionAction, ℝ³, Motions.one, ∅)
  have disjointImages : Disjoint(translate(motionAction, ℝ³,
      (matrixRing(realRing, 3)[1], farPoint), unitBall),
      translate(motionAction, ℝ³, Group.one(Motions), ∅))
    rw [movedEmpty, ← shiftedBall.graph]
    exact Disjoint.empty_right at shiftedBall
  have coverImages : translate(motionAction, ℝ³,
      (matrixRing(realRing, 3)[1], farPoint), unitBall) ∪
      translate(motionAction, ℝ³, Group.one(Motions), ∅) = shiftedBall
    rw [movedEmpty, ← shiftedBall.graph]
    exact union2.right_empty at shiftedBall
  have shift : Equidecomposable(motionAction, Motions, ℝ³, unitBall,
      shiftedBall) :=
    Equidecomposable.of_two_pieces at motionAction, Motions, ℝ³, unitBall,
        shiftedBall,
      unitBall, ∅, (matrixRing(realRing, 3)[1], farPoint),
          Group.one(Motions) with
      action, shiftIn, unitIn, unitBall.subset, emptySubset, emptyDisjoint,
          cover,
      disjointImages, coverImages
  have shiftedB := Equidecomposable.transitive with action, secondB, shift
  have apart := unitBall.shift_disjoint
  have union := Equidecomposable.disjoint_union with action, firstA, shiftedB,
      disjoint, apart
  witness A ∪ B
  constructor
  . exact union2.subset with boundedA, boundedB
  . exact union