-- The ball absorbs its center: unitBall and puncturedBall are
-- equidecomposable under the motions, by a turn about an off-center axis
-- 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.Euclid.Center
import Ball
import Geometry.Absorption.Sphere
import Geometry.Absorption.Pieces

-- Some turn has infinite order, since ℝ is uncountable.
theorem turn.exists_infinite_order
  shows ∃ t ∈ ℝ, ¬(t ∈ turnOrders)
proof
  have countable := turn.infinite_order
  have uncountable := reals.uncountable
  unfold Uncountable at uncountable
  by_contra
  rename this => none
  have cover : ℝ ⊆ turnOrders
    intros t ht
    by_contra
    apply none
    exact ⟨t, ht, this⟩
  have realsCountable := Countable.subset with countable, cover
  exact uncountable with realsCountable

-- One half, and the center c = (1/2, 0, 0) of the orbit of the origin.
def oneHalf : Set := realInvValue(2)

instance oneHalf.real
  shows oneHalf ∈ ℝ
proof
  unfold oneHalf
  typecheck

theorem oneHalf.two
  shows oneHalf * 2 = 1
proof
  have nonzero : (2:R) ≠ 0
    intro equal
    linarith
  have real : (2:R) ∈ ℝ by typecheck
  unfold oneHalf
  exact realInvValue.mul_left at (2:R) with nonzero

defgraph centerPoint (i ∈ 3) : ℝ := pick3(oneHalf, (0:R), (0:R), i)
proof
  have half := oneHalf.real
  have zero : (0:R) ∈ ℝ by typecheck
  exact pick3.real with half, zero, zero, member

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

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

theorem centerPoint.one
  shows centerPoint(1) = (0:R)
proof
  have value := centerPoint.value at 1 with index.one_mem
  rw [value, pick3.one]
  rfl

theorem centerPoint.two
  shows centerPoint(2) = (0:R)
proof
  have value := centerPoint.value at 2 with index.two_mem
  rw [value, pick3.two]
  rfl

-- The motion x ↦ R (x − c) + c = R x + (c − R c) for a rotation R.
def aboutCenter (R : Set) : Set :=
  (R, addVector(centerPoint, vectorNeg(R · centerPoint)))

theorem aboutCenter.graph (R : Set)
  shows aboutCenter(R) =
    (R, addVector(centerPoint, vectorNeg(R · centerPoint)))
proof
  simp [aboutCenter]

theorem centerShift.vector (R : realRing ^ 3 × 3)
  shows addVector(centerPoint, vectorNeg(R · centerPoint)) : 3 → ℝ
proof
  have center := centerPoint.vector
  have image := matrixVector.vector at R, centerPoint with *
  have negated := vectorNeg.vector with image
  exact addVector.vector with center, negated

theorem aboutCenter.member (R : realRing ^ 3 × 3)
  requires hR : R ∈ so3Matrices
  shows aboutCenter(R) ∈ motions
proof
  have shift := centerShift.vector at R with *
  have shiftIn := ℝ³.of_function with shift
  rw aboutCenter.graph
  exact motions.pair with hR, shiftIn

theorem aboutCenter.origin (R : realRing ^ 3 × 3)
  requires hR : R ∈ so3Matrices
  shows motionAction(aboutCenter(R), zeroVector) =
    addVector(centerPoint, vectorNeg(R · centerPoint))
proof
  have shift := centerShift.vector at R with *
  have shiftIn := ℝ³.of_function with shift
  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zeroVector.vector
  have value := motionAction.apply at R,
    addVector(centerPoint, vectorNeg(R · centerPoint)), zeroVector with hR,
        shiftIn, zeroIn
  have killed := matrixVector.zero_vector at R with *
  have unitAdd := addVector.zero_left at
    addVector(centerPoint, vectorNeg(R · centerPoint)) with shift
  rw [aboutCenter.graph, value, killed, unitAdd]
  rfl

-- The motions about c compose as their rotations do.
theorem aboutCenter.mul (R S : realRing ^ 3 × 3)
  requires hR : R ∈ so3Matrices
  requires hS : S ∈ so3Matrices
  shows motionMul(aboutCenter(R), aboutCenter(S)) = aboutCenter(R * S)
proof
  have center := centerPoint.vector
  have product := Matrix.mul_matrix at R, S with *
  have imageR := matrixVector.vector at R, centerPoint with *
  have imageS := matrixVector.vector at S, centerPoint with *
  have imageRS := matrixVector.vector at R * S, centerPoint with *
  have negR := vectorNeg.vector with imageR
  have negS := vectorNeg.vector with imageS
  have negRS := vectorNeg.vector with imageRS
  have shiftR := addVector.vector with center, negR
  have shiftS := addVector.vector with center, negS
  have shiftRIn := ℝ³.of_function with shiftR
  have shiftSIn := ℝ³.of_function with shiftS
  have value := motionMul.apply at R, S,
    addVector(centerPoint, vectorNeg(R · centerPoint)),
    addVector(centerPoint, vectorNeg(S · centerPoint)) with hR, hS, shiftRIn,
        shiftSIn
  have linear := matrixVector.add_vector at R, centerPoint,
      vectorNeg(S · centerPoint)
    with center, negS
  have negLaw := matrixVector.neg at R, S · centerPoint with imageS
  have composed := matrixVector.mul at R, S, centerPoint with center
  have inner := addVector.vector with imageR, negRS
  have comm := addVector.comm at
    addVector(R · centerPoint, vectorNeg((R * S) · centerPoint)),
    addVector(centerPoint, vectorNeg(R · centerPoint)) with inner, shiftR
  have assoc1 := addVector.assoc at centerPoint, vectorNeg(R · centerPoint),
    addVector(R · centerPoint, vectorNeg((R * S) · centerPoint)) with center,
        negR, inner
  have assoc2 := addVector.assoc at vectorNeg(R · centerPoint),
    R · centerPoint, vectorNeg((R * S) · centerPoint)
    with negR, imageR, negRS
  have cancel := addVector.neg_left at R · centerPoint with imageR
  have unitAdd :=
      addVector.zero_left at vectorNeg((R * S) · centerPoint) with negRS
  rw [aboutCenter.graph, aboutCenter.graph, aboutCenter.graph, value, linear,
      negLaw,
    ← composed, comm, assoc1, ← assoc2, cancel, unitAdd]
  rfl

theorem aboutCenter.one
  shows aboutCenter(matrixRing(realRing, 3)[1]) = motionOne
proof
  have one := Matrix.one_matrix
  have center := centerPoint.vector
  have unitAct := matrixVector.one at centerPoint with center
  have cancel := addVector.neg at centerPoint with center
  rw [aboutCenter.graph, unitAct, cancel, motionOne.graph]
  rfl

theorem aboutCenter.pow (R : realRing ^ 3 × 3) (n : Nat)
  requires hR : R ∈ so3Matrices
  shows groupPow(Motions, aboutCenter(R), n) = aboutCenter(groupPow(SO3, R, n))
proof
  induction n
  | zero =>
    have group := Motions.group
    have groupSO3 := SO3.group
    have rhoIn : aboutCenter(R) ∈ Group.carrier(Motions)
      rw Motions.carrierOf
      exact aboutCenter.member with hR
    have rIn : R ∈ Group.carrier(SO3)
      rw SO3.carrierOf
      exact hR
    have unit : groupPow(Motions, aboutCenter(R), 0) = Group.one(Motions) :=
      pow_zero with group, rhoIn
    have unitSO3 : groupPow(SO3, R,
        0) = Group.one(SO3) := pow_zero with groupSO3, rIn
    rw [unit, unitSO3, Motions.oneOf, SO3.oneOf, aboutCenter.one]
    rfl
  | succ(k) using ih =>
    have group := Motions.group
    have groupSO3 := SO3.group
    have rhoIn : aboutCenter(R) ∈ Group.carrier(Motions)
      rw Motions.carrierOf
      exact aboutCenter.member with hR
    have rIn : R ∈ Group.carrier(SO3)
      rw SO3.carrierOf
      exact hR
    have step := pow_succ_left at Motions, aboutCenter(R), k with group
    have stepSO3 := pow_succ_left at SO3, R, k with groupSO3
    have succForm : k + 1 = succ(k) := add.right_one at k
    rw succForm at step
    rw succForm at stepSO3
    have powerIn : groupPow(SO3, R, k) ∈ Group.carrier(SO3) :=
      Group.pow_mem with groupSO3, rIn
    rw SO3.carrierOf at powerIn
    have matrixPower := so3Matrices.matrix with powerIn
    have operation := SO3.product_value with hR, powerIn
    have combine := aboutCenter.mul with hR, powerIn
    rw [step, stepSO3, Motions.mulOf, ih, operation, combine]
    rfl

-- The displacement c − R c of the origin: its entries, its squared norm,
-- its membership in the ball, and its vanishing only for R = 1 among the
-- plane turns.
theorem centerShift.entry (P : realRing ^ 3 × 3) (i : Set)
  requires hi : i ∈ 3
  shows addVector(centerPoint, vectorNeg(P · centerPoint))(i) =
    (centerPoint(i):R) - (P[i, 0]:R) * oneHalf
proof
  have center := centerPoint.vector
  have half := oneHalf.real
  have image := matrixVector.vector at P, centerPoint with *
  have negated := vectorNeg.vector with image
  obtain ⟨p0, p1, p2⟩ := Matrix.row_real at P, i with hi
  have ci := vector.component_real at centerPoint, i with center, hi
  have e1 := addVector.entry at centerPoint, vectorNeg(P · centerPoint), i with
    center, negated, hi
  have e2 := vectorNeg.entry at P · centerPoint, i with image, hi
  have e3 := matrixVector.entry at P, centerPoint, i with *
  have c0 := centerPoint.zero
  have c1 := centerPoint.one
  have c2 := centerPoint.two
  rw [e1, e2, e3, c0, c1, c2]
  ring

theorem centerShift.normSq (P : realRing ^ 3 × 3)
  requires hP : P ∈ so3Matrices
  shows normSq(addVector(centerPoint, vectorNeg(P · centerPoint))) =
    oneHalf * oneHalf * ((2:R) - (2:R) * (P[0, 0]:R))
proof
  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ :=
      Matrix.entries_real with *
  have half := oneHalf.real
  have orthogonal := so3Matrices.orthogonal with hP
  have column := Orthogonal.column_same at P, 0 with orthogonal, index.zero_mem
  have e0 := centerShift.entry at P, 0 with index.zero_mem
  have e1 := centerShift.entry at P, 1 with index.one_mem
  have e2 := centerShift.entry at P, 2 with index.two_mem
  have c0 := centerPoint.zero
  have c1 := centerPoint.one
  have c2 := centerPoint.two
  rw [normSq.value, e0, e1, e2, c0, c1, c2]
  have key : (oneHalf - (P[0, 0]:R) * oneHalf) * (oneHalf - (P[0,
      0]:R) * oneHalf) +
      ((0:R) - (P[1, 0]:R) * oneHalf) * ((0:R) - (P[1, 0]:R) * oneHalf) +
      ((0:R) - (P[2, 0]:R) * oneHalf) * ((0:R) - (P[2, 0]:R) * oneHalf) =
      oneHalf * oneHalf * ((2:R) - (2:R) * (P[0, 0]:R)) +
      oneHalf * oneHalf * ((P[0, 0]:R) * (P[0, 0]:R) + (P[1, 0]:R) * (P[1,
          0]:R) +
        (P[2, 0]:R) * (P[2, 0]:R) - (1:R))
    ring
  rw [key, column]
  ring

theorem centerShift.in_ball (P : realRing ^ 3 × 3)
  requires hP : P ∈ so3Matrices
  shows addVector(centerPoint, vectorNeg(P · centerPoint)) ∈ unitBall
proof
  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ :=
      Matrix.entries_real with *
  have shift := centerShift.vector at P with *
  have shiftIn := ℝ³.of_function with shift
  have orthogonal := so3Matrices.orthogonal with hP
  have column := Orthogonal.column_same at P, 0 with orthogonal, index.zero_mem
  have norm := centerShift.normSq with hP
  have half := oneHalf.real
  have double := oneHalf.two
  have sumReal : (1:R) + (P[0, 0]:R) ∈ ℝ by typecheck
  have sq0 := realMulValue.square_nonnegative at (1:R) + (P[0, 0]:R)
  have sq1 := realMulValue.square_nonnegative at (P[1, 0]:R)
  have sq2 := realMulValue.square_nonnegative at (P[2, 0]:R)
  have sqHalf := realMulValue.square_nonnegative at oneHalf
  have expand : ((1:R) + (P[0, 0]:R)) * ((1:R) + (P[0, 0]:R)) +
      (P[1, 0]:R) * (P[1, 0]:R) + (P[2, 0]:R) * (P[2, 0]:R) =
      (2:R) + (2:R) * (P[0, 0]:R) + ((P[0, 0]:R) * (P[0, 0]:R) +
        (P[1, 0]:R) * (P[1, 0]:R) + (P[2, 0]:R) * (P[2, 0]:R) - (1:R))
    ring
  rw column at expand
  have inner : (2:R) - (2:R) * (P[0, 0]:R) ≤ (4:R) by linarith
  have innerReal : (2:R) - (2:R) * (P[0, 0]:R) ∈ ℝ by typecheck
  have fourReal : (4:R) ∈ ℝ by typecheck
  have squareReal : oneHalf * oneHalf ∈ ℝ by typecheck
  have scaled := realLe.mul_left_of_nonnegative at (2:R) - (2:R) * (P[0,
      0]:R), (4:R),
    oneHalf * oneHalf with inner, sqHalf
  have four : oneHalf * oneHalf * (4:R) = (1:R)
    have regroup : oneHalf * oneHalf * (4:R) = (oneHalf * 2) * (oneHalf * 2)
      ring
    rw [regroup, double]
    ring
  rw four at scaled
  rw ← norm at scaled
  exact unitBall.membership.backward with ⟨shiftIn, scaled⟩

theorem centerShift.nonzero (a b : Real)
  requires zero : addVector(centerPoint, vectorNeg(planeTurn(a,
      b) · centerPoint)) = zeroVector
  shows planeTurn(a, b) = Ring.one(matrixRing(realRing, 3))
proof
  have matrix := planeTurn.matrix at a, b
  have half := oneHalf.real
  have double := oneHalf.two
  have e0 := centerShift.entry at planeTurn(a, b), 0 with index.zero_mem
  have e1 := centerShift.entry at planeTurn(a, b), 1 with index.one_mem
  rw [zero, zeroVector.entry, centerPoint.zero, planeTurn.entry00] at e0
  rw [zero, zeroVector.entry, centerPoint.one, planeTurn.entry10] at e1
  have twiceA : (oneHalf - a * oneHalf) * 2 = (1:R) - a
    have regroup : (oneHalf - a * oneHalf) * 2 = oneHalf * 2 - a * (oneHalf * 2)
      ring
    rw [regroup, double]
    ring
  have twiceB : ((0:R) - b * oneHalf) * 2 = -b
    have regroup : ((0:R) - b * oneHalf) * 2 = (0:R) - b * (oneHalf * 2)
      ring
    rw [regroup, double]
    ring
  rw ← e0 at twiceA
  rw ← e1 at twiceB
  have aOne : a = (1:R) by linarith
  have bZero : b = (0:R) by linarith
  rw [aOne, bZero]
  exact planeTurn.one

-- Every power of a turn is a plane turn by a point of the unit circle.
theorem turn.pow_plane (t : Real) (n : Nat)
  shows ∃ a ∈ ℝ, ∃ b ∈ ℝ,
    matrixPow3(turn(t), n) = planeTurn(a, b) ∧
    (a:R) * (a:R) + (b:R) * (b:R) = (1:R)
proof
  induction n
  | zero =>
    have typed : Matrix3(turn(t)) := Matrix3.of_matrix with (turn.matrix at t)
    have unit := matrixPow3.zero at turn(t) with typed
    have oneReal : (1:R) ∈ ℝ by typecheck
    have zeroReal : (0:R) ∈ ℝ by typecheck
    have shape : matrixPow3(turn(t), 0) = planeTurn((1:R), (0:R))
      rw [unit, planeTurn.one]
      rfl
    have circle : (1:R) * (1:R) + (0:R) * (0:R) = (1:R)
      ring
    exact ⟨(1:R), oneReal, (0:R), zeroReal, shape, circle⟩
  | succ(k) using ih =>
    obtain ⟨a, aReal, b, bReal, shape, circle⟩ := ih
    have typed : Matrix3(turn(t)) := Matrix3.of_matrix with (turn.matrix at t)
    have step := matrixPow3.succ at turn(t), k with typed
    have succForm : k + 1 = succ(k) := add.right_one at k
    rw succForm at step
    have product := planeTurn.mul at turnCos(t), turnSin(t), a, b
    have circleT := turn.circle at t
    have cosReal : turnCos(t) ∈ ℝ by typecheck
    have sinReal : turnSin(t) ∈ ℝ by typecheck
    have newA : turnCos(t) * (a:R) - turnSin(t) * (b:R) ∈ ℝ by typecheck
    have newB : turnCos(t) * (b:R) + turnSin(t) * (a:R) ∈ ℝ by typecheck
    have newShape : matrixPow3(turn(t), succ(k)) =
        planeTurn(turnCos(t) * (a:R) - turnSin(t) * (b:R),
          turnCos(t) * (b:R) + turnSin(t) * (a:R))
      rw [step, shape, turn.graph, product]
      rfl
    have expand : (turnCos(t) * (a:R) - turnSin(t) * (b:R)) *
        (turnCos(t) * (a:R) - turnSin(t) * (b:R)) +
        (turnCos(t) * (b:R) + turnSin(t) * (a:R)) *
        (turnCos(t) * (b:R) + turnSin(t) * (a:R)) =
        (turnCos(t) * turnCos(t) + turnSin(t) * turnSin(t)) *
        ((a:R) * (a:R) + (b:R) * (b:R))
      ring
    have newCircle : (turnCos(t) * (a:R) - turnSin(t) * (b:R)) *
        (turnCos(t) * (a:R) - turnSin(t) * (b:R)) +
        (turnCos(t) * (b:R) + turnSin(t) * (a:R)) *
        (turnCos(t) * (b:R) + turnSin(t) * (a:R)) = (1:R)
      rw [expand, circleT, circle]
      ring
    exact ⟨turnCos(t) * (a:R) - turnSin(t) * (b:R), newA,
      turnCos(t) * (b:R) + turnSin(t) * (a:R), newB, newShape, newCircle⟩

-- The orbit of the origin under the motion about c by turn(t).
def centerOrbit (t : Set) : Set :=
  forwardOrbit(motionAction, Motions, aboutCenter(turn(t)), {zeroVector})

theorem centerOrbit.graph (t : Set)
  shows centerOrbit(t) = forwardOrbit(motionAction, Motions,
      aboutCenter(turn(t)), {zeroVector})
proof
  simp [centerOrbit]

theorem centerTurn.in_ball (t : Real) (n : Nat)
  shows motionAction(groupPow(Motions, aboutCenter(turn(t)), n),
      zeroVector) ∈ unitBall
proof
  have rotation := turn.rotation at t
  have matrix := turn.matrix at t
  have group := SO3.group
  have rotationIn : turn(t) ∈ Group.carrier(SO3)
    rw SO3.carrierOf
    exact rotation
  have powerIn : groupPow(SO3, turn(t), n) ∈ Group.carrier(SO3) :=
    Group.pow_mem with group, rotationIn
  rw SO3.carrierOf at powerIn
  have matrixPower := so3Matrices.matrix with powerIn
  have pow := aboutCenter.pow at turn(t), n with rotation
  have origin := aboutCenter.origin at groupPow(SO3, turn(t), n) with powerIn
  rw [pow, origin]
  exact centerShift.in_ball with powerIn

theorem centerTurn.moves (t : Real) (n : Nat)
  requires generic : ¬(t ∈ turnOrders)
  shows motionAction(groupPow(Motions, aboutCenter(turn(t)), n + 1),
      zeroVector) ≠ zeroVector
proof
  have rotation := turn.rotation at t
  have matrix := turn.matrix at t
  have group := SO3.group
  have rotationIn : turn(t) ∈ Group.carrier(SO3)
    rw SO3.carrierOf
    exact rotation
  have powerIn : groupPow(SO3, turn(t), n + 1) ∈ Group.carrier(SO3) :=
    Group.pow_mem with group, rotationIn
  rw SO3.carrierOf at powerIn
  have pow := aboutCenter.pow at turn(t), n + 1 with rotation
  have matrixPow := turn.groupPow at t, n + 1
  obtain ⟨a, aReal, b, bReal, shape, circle⟩ := turn.pow_plane at t, n + 1
  rw [matrixPow, shape] at powerIn
  have matrixPlane := planeTurn.matrix at a, b
  have origin := aboutCenter.origin at planeTurn(a, b) with powerIn
  rw [pow, matrixPow, shape, origin]
  intro zero
  have unit := centerShift.nonzero with zero
  have power : matrixPow3(turn(t), n + 1) = Ring.one(matrixRing(realRing, 3))
    rw [shape, unit]
    rfl
  have positive : 0 < n + 1 by arith
  have succIn : n + 1 ∈ ℕ by typecheck
  have tReal : t ∈ ℝ by typecheck
  have inOrders : t ∈ turnOrders :=
    turnOrders.membership.backward with
      ⟨tReal, n + 1, succIn, positive, power⟩
  exact generic with inOrders

theorem centerOrbit.subset_ball (t : Real)
  shows centerOrbit(t) ⊆ unitBall
proof
  rw centerOrbit.graph
  intros y hy
  obtain ⟨n, hn, inStage⟩ := forwardOrbit.membership.forward with hy
  obtain ⟨x, hx, shape⟩ := actImage.membership.forward with inStage
  have natural := omega.natural with hn
  have xZero := singleton.membership.forward with hx
  rw [← shape, xZero]
  exact centerTurn.in_ball at t, n

theorem centerTurn.separates (t : Real)
  requires generic : ¬(t ∈ turnOrders)
  shows ∀ n ∈ ℕ, Disjoint(actImage(motionAction,
    groupPow(Motions, aboutCenter(turn(t)), n + 1), {zeroVector}), {zeroVector})
proof
  intros n hn
  have natural := omega.natural with hn
  apply Disjoint.iff.backward
  intros y hy hy2
  obtain ⟨x, hx, shape⟩ := actImage.membership.forward with hy
  have xZero := singleton.membership.forward with hx
  have yZero := singleton.membership.forward with hy2
  have moved := centerTurn.moves at t, n with generic
  apply moved
  cc

-- The ball absorbs its center.
theorem unitBall.absorb_center
  shows Equidecomposable(motionAction, Motions, ℝ³, unitBall, puncturedBall)
proof
  obtain ⟨t, tReal, generic⟩ := turn.exists_infinite_order
  have real : Real(t) by typecheck
  have action := motionAction.action
  have group := Motions.group
  have rotation := turn.rotation at t
  have rhoIn : aboutCenter(turn(t)) ∈ Group.carrier(Motions)
    rw Motions.carrierOf
    exact aboutCenter.member with rotation
  have unitIn : Group.one(Motions) ∈ Group.carrier(Motions) := Group.one_mem
      with group
  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zeroVector.vector
  have subset : {zeroVector} ⊆ ℝ³
    intros x hx
    have equal := singleton.membership.forward with hx
    rw equal
    exact zeroIn
  have separated := centerTurn.separates at t with generic
  have orbitSubset : forwardOrbit(motionAction, Motions, aboutCenter(turn(t)),
      {zeroVector}) ⊆ ℝ³ := forwardOrbit.subset with action, subset
  have orbitContains : {zeroVector} ⊆ forwardOrbit(motionAction, Motions,
      aboutCenter(turn(t)),
          {zeroVector}) := forwardOrbit.contains with action, subset
  have carried := forwardOrbit.image with action, subset, separated
  rw ← centerOrbit.graph at orbitSubset
  rw ← centerOrbit.graph at orbitContains
  rw ← centerOrbit.graph at carried
  have orbitBall := centerOrbit.subset_ball at t
  have restSubset : unitBall ∖ centerOrbit(t) ⊆ ℝ³ :=
    Subset.transitive with (difference.subset_left at unitBall,
        centerOrbit(t)), unitBall.subset
  have disjoint := Disjoint.difference_right at unitBall, centerOrbit(t)
  have cover := difference.union2_of_subset with orbitBall
  have movedOrbit : translate(motionAction, ℝ³, aboutCenter(turn(t)),
      centerOrbit(t)) =
      actImage(motionAction, aboutCenter(turn(t)), centerOrbit(t)) :=
    actImage.eq_translate with action, orbitSubset
  have movedRest : translate(motionAction, ℝ³, Group.one(Motions),
      unitBall ∖ centerOrbit(t)) =
      unitBall ∖ centerOrbit(t) := translate.unit with action, restSubset
  have disjointImages : Disjoint(translate(motionAction, ℝ³,
      aboutCenter(turn(t)), centerOrbit(t)),
      translate(motionAction, ℝ³, Group.one(Motions),
          unitBall ∖ centerOrbit(t)))
    rw [movedOrbit, movedRest, carried]
    apply Disjoint.iff.backward
    intros y hy hy2
    obtain ⟨inOrbit, notZero⟩ := difference.membership.forward with hy
    obtain ⟨inBall, notInOrbit⟩ := difference.membership.forward with hy2
    exact notInOrbit with inOrbit
  have coverImages : translate(motionAction, ℝ³, aboutCenter(turn(t)),
      centerOrbit(t)) ∪
      translate(motionAction, ℝ³, Group.one(Motions),
          unitBall ∖ centerOrbit(t)) =
      unitBall ∖ {zeroVector}
    rw [movedOrbit, movedRest, carried]
    ext y
    constructor
    . intro hy
      have sides := union2.membership.forward with hy
      cases sides with inLeft | inRight
      . obtain ⟨inOrbit, notZero⟩ :=
          difference.membership.forward with inLeft
        have inBall := orbitBall with y, inOrbit
        exact difference.membership.backward with ⟨inBall, notZero⟩
      . obtain ⟨inBall, notInOrbit⟩ := difference.membership.forward
          with inRight
        have notZero : ¬(y ∈ {zeroVector})
          intro inZero
          exact notInOrbit with (orbitContains with y, inZero)
        exact difference.membership.backward with ⟨inBall, notZero⟩
    . intro hy
      obtain ⟨inBall, notZero⟩ := difference.membership.forward with hy
      have alternatives : y ∈ centerOrbit(t) ∨ ¬(y ∈ centerOrbit(t))
        tauto
      apply union2.membership.backward
      cases alternatives with inOrbit | notInOrbit
      . left
        exact difference.membership.backward with ⟨inOrbit, notZero⟩
      . right
        exact difference.membership.backward with ⟨inBall, notInOrbit⟩
  rw puncturedBall.graph
  exact Equidecomposable.of_two_pieces at motionAction, Motions, ℝ³,
    unitBall, unitBall ∖ {zeroVector}, centerOrbit(t),
    unitBall ∖ centerOrbit(t), aboutCenter(turn(t)), Group.one(Motions)
    with action, rhoIn, unitIn, orbitSubset, restSubset, disjoint, cover,
      disjointImages, coverImages