Grace/Cumulus/Geometry/BanachTarski.g17

Open in Workbench Download source

Imports

Sphere · Euclid · Algebra.Group.Paradox.Transfer

Declarations

Source

1-- The Banach–Tarski paradox: the closed unit ball of ℝ³ is paradoxical2-- under the motions, and a part of it is equidecomposable with the3-- disjoint union of two balls; the strong form is in BanachTarski/Strong4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Geometry.BanachTarski10import Sphere11import Euclid12import Algebra.Group.Paradox.Transfer1314-- The punctured ball is paradoxical under the rotations: the two pieces15-- of the sphere lift to their cones.16theorem puncturedBall.pieces17  shows ∃ A, ∃ B, A ⊆ puncturedBall ∧ B ⊆ puncturedBall ∧18    Disjoint(A, B) ∧19    Equidecomposable(spaceAction, SO3, ℝ³, A, puncturedBall) ∧20    Equidecomposable(spaceAction, SO3, ℝ³, B, puncturedBall)21proof22  obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ :=23      sphere.paradoxical24  have whole := Subset.reflexive at S²25  have coneA := cone.subset_punctured with boundedA26  have coneB := cone.subset_punctured with boundedB27  have apart := cone.disjoint with boundedA, boundedB, disjoint28  have liftA := cone.equidecomposable with boundedA, whole, firstA29  have liftB := cone.equidecomposable with boundedB, whole, secondB30  rw cone.sphere at liftA31  rw cone.sphere at liftB32  witness cone(A)33  witness cone(B)34  exact ⟨coneA, coneB, apart, liftA, liftB⟩3536theorem puncturedBall.paradoxical37  shows Paradoxical(restrictAction(spaceAction, SO3, puncturedBall), SO3,38      puncturedBall)39proof40  have action := spaceAction.action41  have pieces := puncturedBall.pieces42  exact Paradoxical.to_restrict with action, puncturedBall.subset_space, pieces4344-- The Banach–Tarski paradox: under the motions, the rotations embed and45-- the center is absorbed, so two disjoint parts of the ball are each46-- equidecomposable with the ball.47theorem banachTarski48  shows ∃ A, ∃ B, A ⊆ unitBall ∧ B ⊆ unitBall ∧ Disjoint(A, B) ∧49    Equidecomposable(motionAction, Motions, ℝ³, A, unitBall) ∧50    Equidecomposable(motionAction, Motions, ℝ³, B, unitBall)51proof52  obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ :=53      puncturedBall.pieces54  have action := motionAction.action55  have action2 := spaceAction.action56  have hom := rotationMotion.hom57  have compatible := rotationMotion.compatible58  have liftA :=59      Equidecomposable.of_hom with action, action2, hom, compatible, firstA60  have liftB :=61      Equidecomposable.of_hom with action, action2, hom, compatible, secondB62  have center := unitBall.absorb_center63  have back := Equidecomposable.symmetric with action, center64  have wholeA := Equidecomposable.transitive with action, liftA, back65  have wholeB := Equidecomposable.transitive with action, liftB, back66  have inA := Subset.transitive with boundedA, puncturedBall.subset67  have inB := Subset.transitive with boundedB, puncturedBall.subset68  witness A69  witness B70  exact ⟨inA, inB, disjoint, wholeA, wholeB⟩7172-- The same pieces, as a paradoxical decomposition of the ball under the73-- action graph restricted to the ball.74theorem banachTarski.restricted75  shows Paradoxical(restrictAction(motionAction, Motions, unitBall), Motions,76      unitBall)77proof78  have action := motionAction.action79  have pieces := banachTarski80  exact Paradoxical.to_restrict with action, unitBall.subset, pieces8182-- The ball translated by (3, 0, 0), disjoint from the ball.83defgraph farPoint (i ∈ 3) : ℝ := pick3((3:R), (0:R), (0:R), i)84proof85  have three : (3:R) ∈ ℝ by typecheck86  have zero : (0:R) ∈ ℝ by typecheck87  exact pick3.real with three, zero, zero, member8889instance farPoint.vector90  shows farPoint : 3 → ℝ91proof92  exact farPoint.function9394theorem farPoint.zero95  shows farPoint(0) = (3:R)96proof97  have value := farPoint.value at 0 with index.zero_mem98  rw [value, pick3.zero]99  rfl100101def shiftedBall : Set :=102  translate(motionAction, ℝ³, (matrixRing(realRing, 3)[1], farPoint),103    unitBall)104105theorem shiftedBall.graph106  shows shiftedBall =107    translate(motionAction, ℝ³, (matrixRing(realRing, 3)[1], farPoint),108      unitBall)109proof110  simp [shiftedBall]111112theorem unitBall.shift_disjoint113  shows Disjoint(unitBall, shiftedBall)114proof115  have one := Matrix.one_matrix116  have oneIn := so3Matrices.one_mem117  have far := farPoint.vector118  have farIn : farPoint ∈ ℝ³ := ℝ³.of_function with far119  apply Disjoint.iff.backward120  intros x hx hx2121  rw shiftedBall.graph at hx2122  obtain ⟨xIn, y, hy, shape⟩ := translate.membership.forward with hx2123  obtain ⟨xSpace, xBound⟩ := unitBall.membership.forward with hx124  obtain ⟨ySpace, yBound⟩ := unitBall.membership.forward with hy125  have vectorX := ℝ³.function with xSpace126  have vectorY := ℝ³.function with ySpace127  have value := motionAction.apply at matrixRing(realRing, 3)[1], farPoint,128      y with129    oneIn, farIn, ySpace130  have unitAct := matrixVector.one at y with vectorY131  rw [value, unitAct] at shape132  have e0 := addVector.entry at y, farPoint, 0 with vectorY, far, index.zero_mem133  rw farPoint.zero at e0134  have x0 : (x(0):R) = (y(0):R) + (3:R)135    rw shape136    exact e0137  have x1 := vector.component_real at x, 1 with vectorX, index.one_mem138  have x2 := vector.component_real at x, 2 with vectorX, index.two_mem139  have y0 := vector.component_real at y, 0 with vectorY, index.zero_mem140  have y1 := vector.component_real at y, 1 with vectorY, index.one_mem141  have y2 := vector.component_real at y, 2 with vectorY, index.two_mem142  have x0Real := vector.component_real at x, 0 with vectorX, index.zero_mem143  have sqX1 := realMulValue.square_nonnegative at (x(1):R)144  have sqX2 := realMulValue.square_nonnegative at (x(2):R)145  have sqY1 := realMulValue.square_nonnegative at (y(1):R)146  have sqY2 := realMulValue.square_nonnegative at (y(2):R)147  rw normSq.value at xBound148  rw normSq.value at yBound149  have sumY : (1:R) + (y(0):R) ∈ ℝ by typecheck150  have sqY := realMulValue.square_nonnegative at (1:R) + (y(0):R)151  have expandY : ((1:R) + (y(0):R)) * ((1:R) + (y(0):R)) =152      (1:R) + (2:R) * (y(0):R) + (y(0):R) * (y(0):R)153    ring154  have lowY : -(1:R) ≤ (y(0):R) by linarith155  have lowX : (2:R) ≤ (x(0):R) by linarith156  have differenceX : (x(0):R) - (2:R) ∈ ℝ by typecheck157  have sqX := realMulValue.square_nonnegative at (x(0):R) - (2:R)158  have expandX : ((x(0):R) - (2:R)) * ((x(0):R) - (2:R)) =159      (x(0):R) * (x(0):R) - (4:R) * (x(0):R) + (4:R)160    ring161  linarith162163-- A part of the ball is equidecomposable with the disjoint union of the164-- ball and its translate.165theorem banachTarski.two_balls_part166  shows ∃ C, C ⊆ unitBall ∧167    Equidecomposable(motionAction, Motions, ℝ³, C, unitBall ∪ shiftedBall)168proof169  obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ :=170      banachTarski171  have action := motionAction.action172  have group := Motions.group173  have one := Matrix.one_matrix174  have oneIn := so3Matrices.one_mem175  have farIn : farPoint ∈ ℝ³ := ℝ³.of_function with farPoint.vector176  have shiftIn : (matrixRing(realRing, 3)[1], farPoint) ∈ Motions.carrier177    rw Motions.carrierOf178    exact motions.pair with oneIn, farIn179  have unitIn : Group.one(Motions) ∈ Group.carrier(Motions) := Group.one_mem180      with group181  have emptySubset : ∅ ⊆ ℝ³ := empty.subset at ℝ³182  have emptyDisjoint : Disjoint(unitBall, ∅) :=183    Disjoint.empty_right at unitBall184  have cover : unitBall ∪ ∅ = unitBall := union2.right_empty at unitBall185  have movedEmpty : translate(motionAction, ℝ³, Motions.one, ∅) = ∅186    apply Subset.antisymmetric187    . intros z hz188      obtain ⟨zIn, w, hw, equal⟩ := translate.membership.forward with hz189      exfalso190      settle with set.empty191    . exact empty.subset at translate(motionAction, ℝ³, Motions.one, ∅)192  have disjointImages : Disjoint(translate(motionAction, ℝ³,193      (matrixRing(realRing, 3)[1], farPoint), unitBall),194      translate(motionAction, ℝ³, Group.one(Motions), ∅))195    rw [movedEmpty, ← shiftedBall.graph]196    exact Disjoint.empty_right at shiftedBall197  have coverImages : translate(motionAction, ℝ³,198      (matrixRing(realRing, 3)[1], farPoint), unitBall) ∪199      translate(motionAction, ℝ³, Group.one(Motions), ∅) = shiftedBall200    rw [movedEmpty, ← shiftedBall.graph]201    exact union2.right_empty at shiftedBall202  have shift : Equidecomposable(motionAction, Motions, ℝ³, unitBall,203      shiftedBall) :=204    Equidecomposable.of_two_pieces at motionAction, Motions, ℝ³, unitBall,205        shiftedBall,206      unitBall, ∅, (matrixRing(realRing, 3)[1], farPoint),207          Group.one(Motions) with208      action, shiftIn, unitIn, unitBall.subset, emptySubset, emptyDisjoint,209          cover,210      disjointImages, coverImages211  have shiftedB := Equidecomposable.transitive with action, secondB, shift212  have apart := unitBall.shift_disjoint213  have union := Equidecomposable.disjoint_union with action, firstA, shiftedB,214      disjoint, apart215  witness A ∪ B216  constructor217  . exact union2.subset with boundedA, boundedB218  . exact union219