Grace/Cumulus/Geometry/Euclid/Center.g17

Open in Workbench Download source

Imports

Ball · Geometry.Absorption.Sphere · Geometry.Absorption.Pieces

Declarations

Source

1-- The ball absorbs its center: unitBall and puncturedBall are2-- equidecomposable under the motions, by a turn about an off-center axis3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Geometry.Euclid.Center9import Ball10import Geometry.Absorption.Sphere11import Geometry.Absorption.Pieces1213-- Some turn has infinite order, since ℝ is uncountable.14theorem turn.exists_infinite_order15  shows ∃ t ∈ ℝ, ¬(t ∈ turnOrders)16proof17  have countable := turn.infinite_order18  have uncountable := reals.uncountable19  unfold Uncountable at uncountable20  by_contra21  rename this => none22  have cover : ℝ ⊆ turnOrders23    intros t ht24    by_contra25    apply none26    exact ⟨t, ht, this⟩27  have realsCountable := Countable.subset with countable, cover28  exact uncountable with realsCountable2930-- One half, and the center c = (1/2, 0, 0) of the orbit of the origin.31def oneHalf : Set := realInvValue(2)3233instance oneHalf.real34  shows oneHalf ∈ ℝ35proof36  unfold oneHalf37  typecheck3839theorem oneHalf.two40  shows oneHalf * 2 = 141proof42  have nonzero : (2:R) ≠ 043    intro equal44    linarith45  have real : (2:R) ∈ ℝ by typecheck46  unfold oneHalf47  exact realInvValue.mul_left at (2:R) with nonzero4849defgraph centerPoint (i ∈ 3) : ℝ := pick3(oneHalf, (0:R), (0:R), i)50proof51  have half := oneHalf.real52  have zero : (0:R) ∈ ℝ by typecheck53  exact pick3.real with half, zero, zero, member5455instance centerPoint.vector56  shows centerPoint : 3 → ℝ57proof58  exact centerPoint.function5960theorem centerPoint.zero61  shows centerPoint(0) = oneHalf62proof63  have value := centerPoint.value at 0 with index.zero_mem64  rw [value, pick3.zero]65  rfl6667theorem centerPoint.one68  shows centerPoint(1) = (0:R)69proof70  have value := centerPoint.value at 1 with index.one_mem71  rw [value, pick3.one]72  rfl7374theorem centerPoint.two75  shows centerPoint(2) = (0:R)76proof77  have value := centerPoint.value at 2 with index.two_mem78  rw [value, pick3.two]79  rfl8081-- The motion x ↦ R (x − c) + c = R x + (c − R c) for a rotation R.82def aboutCenter (R : Set) : Set :=83  (R, addVector(centerPoint, vectorNeg(R · centerPoint)))8485theorem aboutCenter.graph (R : Set)86  shows aboutCenter(R) =87    (R, addVector(centerPoint, vectorNeg(R · centerPoint)))88proof89  simp [aboutCenter]9091theorem centerShift.vector (R : realRing ^ 3 × 3)92  shows addVector(centerPoint, vectorNeg(R · centerPoint)) : 3 → ℝ93proof94  have center := centerPoint.vector95  have image := matrixVector.vector at R, centerPoint with *96  have negated := vectorNeg.vector with image97  exact addVector.vector with center, negated9899theorem aboutCenter.member (R : realRing ^ 3 × 3)100  requires hR : R ∈ so3Matrices101  shows aboutCenter(R) ∈ motions102proof103  have shift := centerShift.vector at R with *104  have shiftIn := ℝ³.of_function with shift105  rw aboutCenter.graph106  exact motions.pair with hR, shiftIn107108theorem aboutCenter.origin (R : realRing ^ 3 × 3)109  requires hR : R ∈ so3Matrices110  shows motionAction(aboutCenter(R), zeroVector) =111    addVector(centerPoint, vectorNeg(R · centerPoint))112proof113  have shift := centerShift.vector at R with *114  have shiftIn := ℝ³.of_function with shift115  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zeroVector.vector116  have value := motionAction.apply at R,117    addVector(centerPoint, vectorNeg(R · centerPoint)), zeroVector with hR,118        shiftIn, zeroIn119  have killed := matrixVector.zero_vector at R with *120  have unitAdd := addVector.zero_left at121    addVector(centerPoint, vectorNeg(R · centerPoint)) with shift122  rw [aboutCenter.graph, value, killed, unitAdd]123  rfl124125-- The motions about c compose as their rotations do.126theorem aboutCenter.mul (R S : realRing ^ 3 × 3)127  requires hR : R ∈ so3Matrices128  requires hS : S ∈ so3Matrices129  shows motionMul(aboutCenter(R), aboutCenter(S)) = aboutCenter(R * S)130proof131  have center := centerPoint.vector132  have product := Matrix.mul_matrix at R, S with *133  have imageR := matrixVector.vector at R, centerPoint with *134  have imageS := matrixVector.vector at S, centerPoint with *135  have imageRS := matrixVector.vector at R * S, centerPoint with *136  have negR := vectorNeg.vector with imageR137  have negS := vectorNeg.vector with imageS138  have negRS := vectorNeg.vector with imageRS139  have shiftR := addVector.vector with center, negR140  have shiftS := addVector.vector with center, negS141  have shiftRIn := ℝ³.of_function with shiftR142  have shiftSIn := ℝ³.of_function with shiftS143  have value := motionMul.apply at R, S,144    addVector(centerPoint, vectorNeg(R · centerPoint)),145    addVector(centerPoint, vectorNeg(S · centerPoint)) with hR, hS, shiftRIn,146        shiftSIn147  have linear := matrixVector.add_vector at R, centerPoint,148      vectorNeg(S · centerPoint)149    with center, negS150  have negLaw := matrixVector.neg at R, S · centerPoint with imageS151  have composed := matrixVector.mul at R, S, centerPoint with center152  have inner := addVector.vector with imageR, negRS153  have comm := addVector.comm at154    addVector(R · centerPoint, vectorNeg((R * S) · centerPoint)),155    addVector(centerPoint, vectorNeg(R · centerPoint)) with inner, shiftR156  have assoc1 := addVector.assoc at centerPoint, vectorNeg(R · centerPoint),157    addVector(R · centerPoint, vectorNeg((R * S) · centerPoint)) with center,158        negR, inner159  have assoc2 := addVector.assoc at vectorNeg(R · centerPoint),160    R · centerPoint, vectorNeg((R * S) · centerPoint)161    with negR, imageR, negRS162  have cancel := addVector.neg_left at R · centerPoint with imageR163  have unitAdd :=164      addVector.zero_left at vectorNeg((R * S) · centerPoint) with negRS165  rw [aboutCenter.graph, aboutCenter.graph, aboutCenter.graph, value, linear,166      negLaw,167    ← composed, comm, assoc1, ← assoc2, cancel, unitAdd]168  rfl169170theorem aboutCenter.one171  shows aboutCenter(matrixRing(realRing, 3)[1]) = motionOne172proof173  have one := Matrix.one_matrix174  have center := centerPoint.vector175  have unitAct := matrixVector.one at centerPoint with center176  have cancel := addVector.neg at centerPoint with center177  rw [aboutCenter.graph, unitAct, cancel, motionOne.graph]178  rfl179180theorem aboutCenter.pow (R : realRing ^ 3 × 3) (n : Nat)181  requires hR : R ∈ so3Matrices182  shows groupPow(Motions, aboutCenter(R), n) = aboutCenter(groupPow(SO3, R, n))183proof184  induction n185  | zero =>186    have group := Motions.group187    have groupSO3 := SO3.group188    have rhoIn : aboutCenter(R) ∈ Group.carrier(Motions)189      rw Motions.carrierOf190      exact aboutCenter.member with hR191    have rIn : R ∈ Group.carrier(SO3)192      rw SO3.carrierOf193      exact hR194    have unit : groupPow(Motions, aboutCenter(R), 0) = Group.one(Motions) :=195      pow_zero with group, rhoIn196    have unitSO3 : groupPow(SO3, R,197        0) = Group.one(SO3) := pow_zero with groupSO3, rIn198    rw [unit, unitSO3, Motions.oneOf, SO3.oneOf, aboutCenter.one]199    rfl200  | succ(k) using ih =>201    have group := Motions.group202    have groupSO3 := SO3.group203    have rhoIn : aboutCenter(R) ∈ Group.carrier(Motions)204      rw Motions.carrierOf205      exact aboutCenter.member with hR206    have rIn : R ∈ Group.carrier(SO3)207      rw SO3.carrierOf208      exact hR209    have step := pow_succ_left at Motions, aboutCenter(R), k with group210    have stepSO3 := pow_succ_left at SO3, R, k with groupSO3211    have succForm : k + 1 = succ(k) := add.right_one at k212    rw succForm at step213    rw succForm at stepSO3214    have powerIn : groupPow(SO3, R, k) ∈ Group.carrier(SO3) :=215      Group.pow_mem with groupSO3, rIn216    rw SO3.carrierOf at powerIn217    have matrixPower := so3Matrices.matrix with powerIn218    have operation := SO3.product_value with hR, powerIn219    have combine := aboutCenter.mul with hR, powerIn220    rw [step, stepSO3, Motions.mulOf, ih, operation, combine]221    rfl222223-- The displacement c − R c of the origin: its entries, its squared norm,224-- its membership in the ball, and its vanishing only for R = 1 among the225-- plane turns.226theorem centerShift.entry (P : realRing ^ 3 × 3) (i : Set)227  requires hi : i ∈ 3228  shows addVector(centerPoint, vectorNeg(P · centerPoint))(i) =229    (centerPoint(i):R) - (P[i, 0]:R) * oneHalf230proof231  have center := centerPoint.vector232  have half := oneHalf.real233  have image := matrixVector.vector at P, centerPoint with *234  have negated := vectorNeg.vector with image235  obtain ⟨p0, p1, p2⟩ := Matrix.row_real at P, i with hi236  have ci := vector.component_real at centerPoint, i with center, hi237  have e1 := addVector.entry at centerPoint, vectorNeg(P · centerPoint), i with238    center, negated, hi239  have e2 := vectorNeg.entry at P · centerPoint, i with image, hi240  have e3 := matrixVector.entry at P, centerPoint, i with *241  have c0 := centerPoint.zero242  have c1 := centerPoint.one243  have c2 := centerPoint.two244  rw [e1, e2, e3, c0, c1, c2]245  ring246247theorem centerShift.normSq (P : realRing ^ 3 × 3)248  requires hP : P ∈ so3Matrices249  shows normSq(addVector(centerPoint, vectorNeg(P · centerPoint))) =250    oneHalf * oneHalf * ((2:R) - (2:R) * (P[0, 0]:R))251proof252  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ :=253      Matrix.entries_real with *254  have half := oneHalf.real255  have orthogonal := so3Matrices.orthogonal with hP256  have column := Orthogonal.column_same at P, 0 with orthogonal, index.zero_mem257  have e0 := centerShift.entry at P, 0 with index.zero_mem258  have e1 := centerShift.entry at P, 1 with index.one_mem259  have e2 := centerShift.entry at P, 2 with index.two_mem260  have c0 := centerPoint.zero261  have c1 := centerPoint.one262  have c2 := centerPoint.two263  rw [normSq.value, e0, e1, e2, c0, c1, c2]264  have key : (oneHalf - (P[0, 0]:R) * oneHalf) * (oneHalf - (P[0,265      0]:R) * oneHalf) +266      ((0:R) - (P[1, 0]:R) * oneHalf) * ((0:R) - (P[1, 0]:R) * oneHalf) +267      ((0:R) - (P[2, 0]:R) * oneHalf) * ((0:R) - (P[2, 0]:R) * oneHalf) =268      oneHalf * oneHalf * ((2:R) - (2:R) * (P[0, 0]:R)) +269      oneHalf * oneHalf * ((P[0, 0]:R) * (P[0, 0]:R) + (P[1, 0]:R) * (P[1,270          0]:R) +271        (P[2, 0]:R) * (P[2, 0]:R) - (1:R))272    ring273  rw [key, column]274  ring275276theorem centerShift.in_ball (P : realRing ^ 3 × 3)277  requires hP : P ∈ so3Matrices278  shows addVector(centerPoint, vectorNeg(P · centerPoint)) ∈ unitBall279proof280  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ :=281      Matrix.entries_real with *282  have shift := centerShift.vector at P with *283  have shiftIn := ℝ³.of_function with shift284  have orthogonal := so3Matrices.orthogonal with hP285  have column := Orthogonal.column_same at P, 0 with orthogonal, index.zero_mem286  have norm := centerShift.normSq with hP287  have half := oneHalf.real288  have double := oneHalf.two289  have sumReal : (1:R) + (P[0, 0]:R) ∈ ℝ by typecheck290  have sq0 := realMulValue.square_nonnegative at (1:R) + (P[0, 0]:R)291  have sq1 := realMulValue.square_nonnegative at (P[1, 0]:R)292  have sq2 := realMulValue.square_nonnegative at (P[2, 0]:R)293  have sqHalf := realMulValue.square_nonnegative at oneHalf294  have expand : ((1:R) + (P[0, 0]:R)) * ((1:R) + (P[0, 0]:R)) +295      (P[1, 0]:R) * (P[1, 0]:R) + (P[2, 0]:R) * (P[2, 0]:R) =296      (2:R) + (2:R) * (P[0, 0]:R) + ((P[0, 0]:R) * (P[0, 0]:R) +297        (P[1, 0]:R) * (P[1, 0]:R) + (P[2, 0]:R) * (P[2, 0]:R) - (1:R))298    ring299  rw column at expand300  have inner : (2:R) - (2:R) * (P[0, 0]:R) ≤ (4:R) by linarith301  have innerReal : (2:R) - (2:R) * (P[0, 0]:R) ∈ ℝ by typecheck302  have fourReal : (4:R) ∈ ℝ by typecheck303  have squareReal : oneHalf * oneHalf ∈ ℝ by typecheck304  have scaled := realLe.mul_left_of_nonnegative at (2:R) - (2:R) * (P[0,305      0]:R), (4:R),306    oneHalf * oneHalf with inner, sqHalf307  have four : oneHalf * oneHalf * (4:R) = (1:R)308    have regroup : oneHalf * oneHalf * (4:R) = (oneHalf * 2) * (oneHalf * 2)309      ring310    rw [regroup, double]311    ring312  rw four at scaled313  rw ← norm at scaled314  exact unitBall.membership.backward with ⟨shiftIn, scaled⟩315316theorem centerShift.nonzero (a b : Real)317  requires zero : addVector(centerPoint, vectorNeg(planeTurn(a,318      b) · centerPoint)) = zeroVector319  shows planeTurn(a, b) = Ring.one(matrixRing(realRing, 3))320proof321  have matrix := planeTurn.matrix at a, b322  have half := oneHalf.real323  have double := oneHalf.two324  have e0 := centerShift.entry at planeTurn(a, b), 0 with index.zero_mem325  have e1 := centerShift.entry at planeTurn(a, b), 1 with index.one_mem326  rw [zero, zeroVector.entry, centerPoint.zero, planeTurn.entry00] at e0327  rw [zero, zeroVector.entry, centerPoint.one, planeTurn.entry10] at e1328  have twiceA : (oneHalf - a * oneHalf) * 2 = (1:R) - a329    have regroup : (oneHalf - a * oneHalf) * 2 = oneHalf * 2 - a * (oneHalf * 2)330      ring331    rw [regroup, double]332    ring333  have twiceB : ((0:R) - b * oneHalf) * 2 = -b334    have regroup : ((0:R) - b * oneHalf) * 2 = (0:R) - b * (oneHalf * 2)335      ring336    rw [regroup, double]337    ring338  rw ← e0 at twiceA339  rw ← e1 at twiceB340  have aOne : a = (1:R) by linarith341  have bZero : b = (0:R) by linarith342  rw [aOne, bZero]343  exact planeTurn.one344345-- Every power of a turn is a plane turn by a point of the unit circle.346theorem turn.pow_plane (t : Real) (n : Nat)347  shows ∃ a ∈ ℝ, ∃ b ∈ ℝ,348    matrixPow3(turn(t), n) = planeTurn(a, b) ∧349    (a:R) * (a:R) + (b:R) * (b:R) = (1:R)350proof351  induction n352  | zero =>353    have typed : Matrix3(turn(t)) := Matrix3.of_matrix with (turn.matrix at t)354    have unit := matrixPow3.zero at turn(t) with typed355    have oneReal : (1:R) ∈ ℝ by typecheck356    have zeroReal : (0:R) ∈ ℝ by typecheck357    have shape : matrixPow3(turn(t), 0) = planeTurn((1:R), (0:R))358      rw [unit, planeTurn.one]359      rfl360    have circle : (1:R) * (1:R) + (0:R) * (0:R) = (1:R)361      ring362    exact ⟨(1:R), oneReal, (0:R), zeroReal, shape, circle⟩363  | succ(k) using ih =>364    obtain ⟨a, aReal, b, bReal, shape, circle⟩ := ih365    have typed : Matrix3(turn(t)) := Matrix3.of_matrix with (turn.matrix at t)366    have step := matrixPow3.succ at turn(t), k with typed367    have succForm : k + 1 = succ(k) := add.right_one at k368    rw succForm at step369    have product := planeTurn.mul at turnCos(t), turnSin(t), a, b370    have circleT := turn.circle at t371    have cosReal : turnCos(t) ∈ ℝ by typecheck372    have sinReal : turnSin(t) ∈ ℝ by typecheck373    have newA : turnCos(t) * (a:R) - turnSin(t) * (b:R) ∈ ℝ by typecheck374    have newB : turnCos(t) * (b:R) + turnSin(t) * (a:R) ∈ ℝ by typecheck375    have newShape : matrixPow3(turn(t), succ(k)) =376        planeTurn(turnCos(t) * (a:R) - turnSin(t) * (b:R),377          turnCos(t) * (b:R) + turnSin(t) * (a:R))378      rw [step, shape, turn.graph, product]379      rfl380    have expand : (turnCos(t) * (a:R) - turnSin(t) * (b:R)) *381        (turnCos(t) * (a:R) - turnSin(t) * (b:R)) +382        (turnCos(t) * (b:R) + turnSin(t) * (a:R)) *383        (turnCos(t) * (b:R) + turnSin(t) * (a:R)) =384        (turnCos(t) * turnCos(t) + turnSin(t) * turnSin(t)) *385        ((a:R) * (a:R) + (b:R) * (b:R))386      ring387    have newCircle : (turnCos(t) * (a:R) - turnSin(t) * (b:R)) *388        (turnCos(t) * (a:R) - turnSin(t) * (b:R)) +389        (turnCos(t) * (b:R) + turnSin(t) * (a:R)) *390        (turnCos(t) * (b:R) + turnSin(t) * (a:R)) = (1:R)391      rw [expand, circleT, circle]392      ring393    exact ⟨turnCos(t) * (a:R) - turnSin(t) * (b:R), newA,394      turnCos(t) * (b:R) + turnSin(t) * (a:R), newB, newShape, newCircle⟩395396-- The orbit of the origin under the motion about c by turn(t).397def centerOrbit (t : Set) : Set :=398  forwardOrbit(motionAction, Motions, aboutCenter(turn(t)), {zeroVector})399400theorem centerOrbit.graph (t : Set)401  shows centerOrbit(t) = forwardOrbit(motionAction, Motions,402      aboutCenter(turn(t)), {zeroVector})403proof404  simp [centerOrbit]405406theorem centerTurn.in_ball (t : Real) (n : Nat)407  shows motionAction(groupPow(Motions, aboutCenter(turn(t)), n),408      zeroVector) ∈ unitBall409proof410  have rotation := turn.rotation at t411  have matrix := turn.matrix at t412  have group := SO3.group413  have rotationIn : turn(t) ∈ Group.carrier(SO3)414    rw SO3.carrierOf415    exact rotation416  have powerIn : groupPow(SO3, turn(t), n) ∈ Group.carrier(SO3) :=417    Group.pow_mem with group, rotationIn418  rw SO3.carrierOf at powerIn419  have matrixPower := so3Matrices.matrix with powerIn420  have pow := aboutCenter.pow at turn(t), n with rotation421  have origin := aboutCenter.origin at groupPow(SO3, turn(t), n) with powerIn422  rw [pow, origin]423  exact centerShift.in_ball with powerIn424425theorem centerTurn.moves (t : Real) (n : Nat)426  requires generic : ¬(t ∈ turnOrders)427  shows motionAction(groupPow(Motions, aboutCenter(turn(t)), n + 1),428      zeroVector) ≠ zeroVector429proof430  have rotation := turn.rotation at t431  have matrix := turn.matrix at t432  have group := SO3.group433  have rotationIn : turn(t) ∈ Group.carrier(SO3)434    rw SO3.carrierOf435    exact rotation436  have powerIn : groupPow(SO3, turn(t), n + 1) ∈ Group.carrier(SO3) :=437    Group.pow_mem with group, rotationIn438  rw SO3.carrierOf at powerIn439  have pow := aboutCenter.pow at turn(t), n + 1 with rotation440  have matrixPow := turn.groupPow at t, n + 1441  obtain ⟨a, aReal, b, bReal, shape, circle⟩ := turn.pow_plane at t, n + 1442  rw [matrixPow, shape] at powerIn443  have matrixPlane := planeTurn.matrix at a, b444  have origin := aboutCenter.origin at planeTurn(a, b) with powerIn445  rw [pow, matrixPow, shape, origin]446  intro zero447  have unit := centerShift.nonzero with zero448  have power : matrixPow3(turn(t), n + 1) = Ring.one(matrixRing(realRing, 3))449    rw [shape, unit]450    rfl451  have positive : 0 < n + 1 by arith452  have succIn : n + 1 ∈ ℕ by typecheck453  have tReal : t ∈ ℝ by typecheck454  have inOrders : t ∈ turnOrders :=455    turnOrders.membership.backward with456      ⟨tReal, n + 1, succIn, positive, power⟩457  exact generic with inOrders458459theorem centerOrbit.subset_ball (t : Real)460  shows centerOrbit(t) ⊆ unitBall461proof462  rw centerOrbit.graph463  intros y hy464  obtain ⟨n, hn, inStage⟩ := forwardOrbit.membership.forward with hy465  obtain ⟨x, hx, shape⟩ := actImage.membership.forward with inStage466  have natural := omega.natural with hn467  have xZero := singleton.membership.forward with hx468  rw [← shape, xZero]469  exact centerTurn.in_ball at t, n470471theorem centerTurn.separates (t : Real)472  requires generic : ¬(t ∈ turnOrders)473  shows ∀ n ∈ ℕ, Disjoint(actImage(motionAction,474    groupPow(Motions, aboutCenter(turn(t)), n + 1), {zeroVector}), {zeroVector})475proof476  intros n hn477  have natural := omega.natural with hn478  apply Disjoint.iff.backward479  intros y hy hy2480  obtain ⟨x, hx, shape⟩ := actImage.membership.forward with hy481  have xZero := singleton.membership.forward with hx482  have yZero := singleton.membership.forward with hy2483  have moved := centerTurn.moves at t, n with generic484  apply moved485  cc486487-- The ball absorbs its center.488theorem unitBall.absorb_center489  shows Equidecomposable(motionAction, Motions, ℝ³, unitBall, puncturedBall)490proof491  obtain ⟨t, tReal, generic⟩ := turn.exists_infinite_order492  have real : Real(t) by typecheck493  have action := motionAction.action494  have group := Motions.group495  have rotation := turn.rotation at t496  have rhoIn : aboutCenter(turn(t)) ∈ Group.carrier(Motions)497    rw Motions.carrierOf498    exact aboutCenter.member with rotation499  have unitIn : Group.one(Motions) ∈ Group.carrier(Motions) := Group.one_mem500      with group501  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zeroVector.vector502  have subset : {zeroVector} ⊆ ℝ³503    intros x hx504    have equal := singleton.membership.forward with hx505    rw equal506    exact zeroIn507  have separated := centerTurn.separates at t with generic508  have orbitSubset : forwardOrbit(motionAction, Motions, aboutCenter(turn(t)),509      {zeroVector}) ⊆ ℝ³ := forwardOrbit.subset with action, subset510  have orbitContains : {zeroVector} ⊆ forwardOrbit(motionAction, Motions,511      aboutCenter(turn(t)),512          {zeroVector}) := forwardOrbit.contains with action, subset513  have carried := forwardOrbit.image with action, subset, separated514  rw ← centerOrbit.graph at orbitSubset515  rw ← centerOrbit.graph at orbitContains516  rw ← centerOrbit.graph at carried517  have orbitBall := centerOrbit.subset_ball at t518  have restSubset : unitBall ∖ centerOrbit(t) ⊆ ℝ³ :=519    Subset.transitive with (difference.subset_left at unitBall,520        centerOrbit(t)), unitBall.subset521  have disjoint := Disjoint.difference_right at unitBall, centerOrbit(t)522  have cover := difference.union2_of_subset with orbitBall523  have movedOrbit : translate(motionAction, ℝ³, aboutCenter(turn(t)),524      centerOrbit(t)) =525      actImage(motionAction, aboutCenter(turn(t)), centerOrbit(t)) :=526    actImage.eq_translate with action, orbitSubset527  have movedRest : translate(motionAction, ℝ³, Group.one(Motions),528      unitBall ∖ centerOrbit(t)) =529      unitBall ∖ centerOrbit(t) := translate.unit with action, restSubset530  have disjointImages : Disjoint(translate(motionAction, ℝ³,531      aboutCenter(turn(t)), centerOrbit(t)),532      translate(motionAction, ℝ³, Group.one(Motions),533          unitBall ∖ centerOrbit(t)))534    rw [movedOrbit, movedRest, carried]535    apply Disjoint.iff.backward536    intros y hy hy2537    obtain ⟨inOrbit, notZero⟩ := difference.membership.forward with hy538    obtain ⟨inBall, notInOrbit⟩ := difference.membership.forward with hy2539    exact notInOrbit with inOrbit540  have coverImages : translate(motionAction, ℝ³, aboutCenter(turn(t)),541      centerOrbit(t)) ∪542      translate(motionAction, ℝ³, Group.one(Motions),543          unitBall ∖ centerOrbit(t)) =544      unitBall ∖ {zeroVector}545    rw [movedOrbit, movedRest, carried]546    ext y547    constructor548    . intro hy549      have sides := union2.membership.forward with hy550      cases sides with inLeft | inRight551      . obtain ⟨inOrbit, notZero⟩ :=552          difference.membership.forward with inLeft553        have inBall := orbitBall with y, inOrbit554        exact difference.membership.backward with ⟨inBall, notZero⟩555      . obtain ⟨inBall, notInOrbit⟩ := difference.membership.forward556          with inRight557        have notZero : ¬(y ∈ {zeroVector})558          intro inZero559          exact notInOrbit with (orbitContains with y, inZero)560        exact difference.membership.backward with ⟨inBall, notZero⟩561    . intro hy562      obtain ⟨inBall, notZero⟩ := difference.membership.forward with hy563      have alternatives : y ∈ centerOrbit(t) ∨ ¬(y ∈ centerOrbit(t))564        tauto565      apply union2.membership.backward566      cases alternatives with inOrbit | notInOrbit567      . left568        exact difference.membership.backward with ⟨inOrbit, notZero⟩569      . right570        exact difference.membership.backward with ⟨inBall, notInOrbit⟩571  rw puncturedBall.graph572  exact Equidecomposable.of_two_pieces at motionAction, Motions, ℝ³,573    unitBall, unitBall ∖ {zeroVector}, centerOrbit(t),574    unitBall ∖ centerOrbit(t), aboutCenter(turn(t)), Group.one(Motions)575    with action, rhoIn, unitIn, orbitSubset, restSubset, disjoint, cover,576      disjointImages, coverImages577