Grace/Cumulus/Geometry/Sphere/Absorb.g17

Open in Workbench Download source

Imports

Transitive · Conjugate · Geometry.Absorption.Final

Declarations

Source

1-- The sphere absorbs any countable subset: S² and S² ∖ D are2-- SO3-equidecomposable for every countable D ⊆ S²3-- 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.Sphere.Absorb9import Transitive10import Conjugate11import Geometry.Absorption.Final1213-- The values of a row of three reals, and rows of unit norm on the sphere.14theorem row3.zero (a b c : Real)15  shows row3(a, b, c)(0) = a16proof17  rw row3.graph18  exact triple.zero at ℝ, a, b, c with *1920theorem row3.one (a b c : Real)21  shows row3(a, b, c)(1) = b22proof23  rw row3.graph24  exact triple.one at ℝ, a, b, c with *2526theorem row3.two (a b c : Real)27  shows row3(a, b, c)(2) = c28proof29  rw row3.graph30  exact triple.two at ℝ, a, b, c with *3132instance row3.function (a b c : Real)33  shows row3(a, b, c) : 3 → ℝ34proof35  have member := row3.member at a, b, c36  exact functionSpace.mem_iff.forward with member3738theorem row3.sphere (a b c : Real)39  requires unit : a * a + b * b + c * c = 140  shows row3(a, b, c) ∈ S²41proof42  have function := row3.function at a, b, c43  have inSpace := ℝ³.of_function with function44  have v0 := row3.zero at a, b, c45  have v1 := row3.one at a, b, c46  have v2 := row3.two at a, b, c47  have norm : normSq(row3(a, b, c)) = (1:R)48    rw [normSq.value, v0, v1, v2]49    exact unit50  exact S².membership.backward with ⟨inSpace, norm⟩5152-- The north pole as a row.53theorem basis.two54  shows basis(2) = row3((0:R), (0:R), (1:R))55proof56  have pole := basis.vector at 2 with index.two_mem57  have row := row3.function at (0:R), (0:R), (1:R)58  apply FunctionBetween.ext with pole, row59  intros i hi60  have alternatives := index.cases with hi61  rcases alternatives with at0 | at1 | at262  . have other := basis.other at 0, 263      with index.zero_mem, index.two_mem, index.zero_ne_two64    rw [at0, other, row3.zero]65    rfl66  . have other := basis.other at 1, 267      with index.one_mem, index.two_mem, index.one_ne_two68    rw [at1, other, row3.one]69    rfl70  . have same := basis.same at 2 with index.two_mem71    rw [at2, same, row3.two]72    rfl7374-- A point of the sphere on the z-axis is one of the two poles.75theorem sphere.axis_cases (v : Set)76  requires sphere : v ∈ S²77  requires axis : vectorPoint(v) = complexZero78  shows v = row3((0:R), (0:R), (1:R)) ∨ v = row3((0:R), (0:R), -(1:R))79proof80  have vector := S².function with sphere81  have v0 := vector.component_real at v, 0 with vector, index.zero_mem82  have v1 := vector.component_real at v, 1 with vector, index.one_mem83  have v2 := vector.component_real at v, 2 with vector, index.two_mem84  obtain ⟨inSpace, unit⟩ := S².membership.forward with sphere85  rw normSq.value at unit86  rw vectorPoint.graph at axis87  unfold complexZero at axis88  obtain ⟨first, second⟩ := orderedPair.injective with axis89  rw [first, second] at unit90  have square : (v(2):R) * (v(2):R) = 191    linear_combination unit92  have alternatives : (v(2):R) = (1:R) ∨ (v(2):R) ≠ (1:R) by tauto93  cases alternatives with north | south94  . left95    have row := row3.function at (0:R), (0:R), (1:R)96    apply FunctionBetween.ext with vector, row97    intros i hi98    have cases := index.cases with hi99    rcases cases with at0 | at1 | at2100    . rw [at0, first, row3.zero]101      rfl102    . rw [at1, second, row3.one]103      rfl104    . rw [at2, north, row3.two]105      rfl106  . right107    have nonzero : (v(2):R) - 1 ≠ 0108      intro zero109      apply south110      linarith111    have factored : ((v(2):R) + 1) * ((v(2):R) - 1) = 0 * ((v(2):R) - 1)112      linear_combination square113    have sum := realMulValue.right_cancel_of_nonzero at (v(2):R) + 1, (0:R),114      (v(2):R) - 1 with nonzero, factored115    have third : (v(2):R) = -(1:R) by linarith116    have row := row3.function at (0:R), (0:R), -(1:R)117    apply FunctionBetween.ext with vector, row118    intros i hi119    have cases := index.cases with hi120    rcases cases with at0 | at1 | at2121    . rw [at0, first, row3.zero]122      rfl123    . rw [at1, second, row3.one]124      rfl125    . rw [at2, third, row3.two]126      rfl127128-- A rotation is undone by its transpose, and carries opposite vectors129-- to opposite vectors.130theorem matrixVector.transpose_cancel (σ v : Set)131  requires rotation : σ ∈ so3Matrices132  requires vector : v : 3 → ℝ133  shows transpose(σ) · (σ · v) = v134proof135  have matrix := so3Matrices.matrix with rotation136  have transposed := transpose.matrix at σ with matrix137  have orthogonal := so3Matrices.orthogonal with rotation138  have left := Orthogonal.left with orthogonal139  have merged := matrixVector.mul at transpose(σ), σ, v with vector140  rw [← merged, left]141  exact matrixVector.one with vector142143theorem matrixVector.opposite (M : realRing ^ 3 × 3) (u v : Set)144  requires vectorU : u : 3 → ℝ145  requires vectorV : v : 3 → ℝ146  requires opposite : ∀ i ∈ 3, (v(i):R) = -(u(i):R)147  shows ∀ i ∈ 3, ((M · v)(i):R) = -((M · u)(i):R)148proof149  intros i hi150  have entryU := matrixVector.entry at M, u, i with *151  have entryV := matrixVector.entry at M, v, i with *152  have o0 := opposite with 0, index.zero_mem153  have o1 := opposite with 1, index.one_mem154  have o2 := opposite with 2, index.two_mem155  obtain ⟨m0, m1, m2⟩ := Matrix.row_real at M, i with hi156  have u0 := vector.component_real at u, 0 with vectorU, index.zero_mem157  have u1 := vector.component_real at u, 1 with vectorU, index.one_mem158  have u2 := vector.component_real at u, 2 with vectorU, index.two_mem159  rw [entryU, entryV, o0, o1, o2]160  ring161162-- The equator, parametrized rationally by the turn, and its antipodes.163defgraph equatorPoint (t ∈ ℝ) : S² := row3(turnCos(t), turnSin(t), (0:R))164proof165  have typed : Real(t) by typecheck166  have circle := turn.circle at t167  have unit : turnCos(t) * turnCos(t) + turnSin(t) * turnSin(t) +168      (0:R) * (0:R) = 1169    linear_combination circle170  exact row3.sphere with unit171172defgraph equatorAntipode (t ∈ ℝ) : S² :=173  row3(-turnCos(t), -turnSin(t), (0:R))174proof175  have typed : Real(t) by typecheck176  have circle := turn.circle at t177  have unit : -turnCos(t) * -turnCos(t) + -turnSin(t) * -turnSin(t) +178      (0:R) * (0:R) = 1179    linear_combination circle180  exact row3.sphere with unit181182theorem equatorPoint.cancel (s t : Real)183  requires same : equatorPoint(s) = equatorPoint(t)184  shows s = t185proof186  have realS : s ∈ ℝ by typecheck187  have realT : t ∈ ℝ by typecheck188  have valueS := equatorPoint.value at s with *189  have valueT := equatorPoint.value at t with *190  rw [valueS, valueT] at same191  have cosS := row3.zero at turnCos(s), turnSin(s), (0:R)192  have cosT := row3.zero at turnCos(t), turnSin(t), (0:R)193  have sinS := row3.one at turnCos(s), turnSin(s), (0:R)194  have sinT := row3.one at turnCos(t), turnSin(t), (0:R)195  have cosEqual : turnCos(s) = turnCos(t) by cc196  have sinEqual : turnSin(s) = turnSin(t) by cc197  exact turn.injective_of_coordinates with cosEqual, sinEqual198199theorem equatorAntipode.cancel (s t : Real)200  requires same : equatorAntipode(s) = equatorAntipode(t)201  shows s = t202proof203  have realS : s ∈ ℝ by typecheck204  have realT : t ∈ ℝ by typecheck205  have valueS := equatorAntipode.value at s with *206  have valueT := equatorAntipode.value at t with *207  rw [valueS, valueT] at same208  have cosS := row3.zero at -turnCos(s), -turnSin(s), (0:R)209  have cosT := row3.zero at -turnCos(t), -turnSin(t), (0:R)210  have sinS := row3.one at -turnCos(s), -turnSin(s), (0:R)211  have sinT := row3.one at -turnCos(t), -turnSin(t), (0:R)212  have cosOpposite : -turnCos(s) = -turnCos(t) by cc213  have sinOpposite : -turnSin(s) = -turnSin(t) by cc214  have cosEqual : turnCos(s) = turnCos(t) by linarith215  have sinEqual : turnSin(s) = turnSin(t) by linarith216  exact turn.injective_of_coordinates with cosEqual, sinEqual217218theorem equatorAntipode.opposite (t : Real)219  shows ∀ i ∈ 3, (equatorAntipode(t)(i):R) = -(equatorPoint(t)(i):R)220proof221  have real : t ∈ ℝ by typecheck222  have valueP := equatorPoint.value at t with *223  have valueA := equatorAntipode.value at t with *224  intros i hi225  rw [valueP, valueA]226  have alternatives := index.cases with hi227  rcases alternatives with at0 | at1 | at2228  . rw [at0, row3.zero, row3.zero]229    rfl230  . rw [at1, row3.one, row3.one]231    rfl232  . rw [at2, row3.two, row3.two]233    ring234235-- The parameters whose point, or whose antipode, lies in D.236def equatorBad (D : Set) : Set := functionPreimage(equatorPoint, ℝ, D)237def antipodeBad (D : Set) : Set := functionPreimage(equatorAntipode, ℝ, D)238239theorem equatorBad.membership (D t : Set)240  shows t ∈ equatorBad(D) ↔ t ∈ ℝ ∧ equatorPoint(t) ∈ D241proof242  simp [equatorBad, functionPreimage.membership]243244theorem antipodeBad.membership (D t : Set)245  shows t ∈ antipodeBad(D) ↔ t ∈ ℝ ∧ equatorAntipode(t) ∈ D246proof247  simp [antipodeBad, functionPreimage.membership]248249theorem equatorBad.countable (D : Set)250  requires countable : Countable(D)251  shows Countable(equatorBad(D))252proof253  have function := equatorPoint.function254  have subset : equatorBad(D) ⊆ ℝ255    intros t ht256    obtain ⟨real, inD⟩ := equatorBad.membership.forward with ht257    exact real258  have closed : ∀ t ∈ equatorBad(D), equatorPoint(t) ∈ D259    intros t ht260    obtain ⟨real, inD⟩ := equatorBad.membership.forward with ht261    exact inD262  have restricted := restrict.function at equatorPoint, ℝ, S²,263    equatorBad(D), D with function, subset, closed264  have injective : InjectiveBetween(restrict(equatorPoint, equatorBad(D)),265      equatorBad(D), D)266    apply Injective.of_pointwise with restricted267    intros s hs t ht same268    have realS := subset with s, hs269    have realT := subset with t, ht270    have typedS : Real(s) by typecheck271    have typedT : Real(t) by typecheck272    have stepS := restrict.apply at equatorPoint, ℝ, S², equatorBad(D), D, s273      with function, subset, closed, hs274    have stepT := restrict.apply at equatorPoint, ℝ, S², equatorBad(D), D, t275      with function, subset, closed, ht276    rw [stepS, stepT] at same277    exact equatorPoint.cancel with same278  exact Countable.of_injection with injective, countable279280theorem antipodeBad.countable (D : Set)281  requires countable : Countable(D)282  shows Countable(antipodeBad(D))283proof284  have function := equatorAntipode.function285  have subset : antipodeBad(D) ⊆ ℝ286    intros t ht287    obtain ⟨real, inD⟩ := antipodeBad.membership.forward with ht288    exact real289  have closed : ∀ t ∈ antipodeBad(D), equatorAntipode(t) ∈ D290    intros t ht291    obtain ⟨real, inD⟩ := antipodeBad.membership.forward with ht292    exact inD293  have restricted := restrict.function at equatorAntipode, ℝ, S²,294    antipodeBad(D), D with function, subset, closed295  have injective : InjectiveBetween(restrict(equatorAntipode, antipodeBad(D)),296      antipodeBad(D), D)297    apply Injective.of_pointwise with restricted298    intros s hs t ht same299    have realS := subset with s, hs300    have realT := subset with t, ht301    have typedS : Real(s) by typecheck302    have typedT : Real(t) by typecheck303    have stepS := restrict.apply at equatorAntipode, ℝ, S², antipodeBad(D),304      D, s with function, subset, closed, hs305    have stepT := restrict.apply at equatorAntipode, ℝ, S², antipodeBad(D),306      D, t with function, subset, closed, ht307    rw [stepS, stepT] at same308    exact equatorAntipode.cancel with same309  exact Countable.of_injection with injective, countable310311-- Some point of the equator lies, with its antipode, outside a countable D.312theorem equator.exists_outside (D : Set)313  requires countable : Countable(D)314  shows ∃ t ∈ ℝ, ¬(equatorPoint(t) ∈ D) ∧315    ¬(equatorAntipode(t) ∈ D)316proof317  have badPoints := equatorBad.countable with countable318  have badAntipodes := antipodeBad.countable with countable319  have bad := Countable.union2 with badPoints, badAntipodes320  have uncountable := reals.uncountable321  unfold Uncountable at uncountable322  by_contra323  rename this => none324  have cover : ℝ ⊆ equatorBad(D) ∪ antipodeBad(D)325    intros t ht326    by_contra327    rename this => outside328    apply none329    refine ⟨t, ht, ?_, ?_⟩330    . intro inD331      apply outside332      have member : t ∈ equatorBad(D) :=333        equatorBad.membership.backward with ⟨ht, inD⟩334      exact union2.left with member335    . intro inD336      apply outside337      have member : t ∈ antipodeBad(D) :=338        antipodeBad.membership.backward with ⟨ht, inD⟩339      exact union2.right with member340  have realsCountable := Countable.subset with bad, cover341  exact uncountable with realsCountable342343-- The image of a countable subset of the sphere under a rotation is344-- countable: it is the image of D under the rotation as a function on S².345defgraph rotateSphere (σ : Set) (v ∈ S²) : S² := σ · v346requires rotation : σ ∈ so3Matrices347proof348  obtain ⟨subset, closed⟩ := Invariant.sphere349  exact closed with σ, rotation, v, member350351theorem actImage.countable (σ D : Set)352  requires rotation : σ ∈ so3Matrices353  requires subset : D ⊆ S²354  requires countable : Countable(D)355  shows Countable(actImage(sphereAction, σ, D))356proof357  have function := rotateSphere.function at σ with rotation358  have closed : ∀ d ∈ D, rotateSphere(σ)(d) ∈ S²359    intros d hd360    exact FunctionBetween.apply_closed with function, (subset with d, hd)361  have restricted := restrict.function at rotateSphere(σ), S², S², D, S²362    with function, subset, closed363  have image := Countable.image at restrict(rotateSphere(σ), D), D, S²364    with restricted, countable365  have bounded : actImage(sphereAction, σ, D) ⊆366      functionImage(restrict(rotateSphere(σ), D), D, S²)367    intros y hy368    obtain ⟨d, hd, moved⟩ := actImage.membership.forward with hy369    have dIn := subset with d, hd370    have applied := sphereAction.apply with rotation, dIn371    have value := rotateSphere.value at σ, d with *372    have step := restrict.apply at rotateSphere(σ), S², S², D, S², d373      with function, subset, closed, hd374    have member := functionImage.value at restrict(rotateSphere(σ), D), D,375      S², d with restricted, hd376    rw [step, value] at member377    rw [← moved, applied]378    exact member379  exact Countable.subset with image, bounded380381-- A rotation carrying the equator point q to the north pole carries its382-- antipode to the south pole, so a point of D off q and -q leaves the axis.383theorem equatorAntipode.image (σ t : Set)384  requires rotation : σ ∈ so3Matrices385  requires real : t ∈ ℝ386  requires pole : σ · equatorPoint(t) = basis(2)387  shows σ · equatorAntipode(t) = row3((0:R), (0:R), -(1:R))388proof389  have typed : Real(t) by typecheck390  have matrix := so3Matrices.matrix with rotation391  have pointIn := FunctionBetween.apply_closed with equatorPoint.function, real392  have antipodeIn := FunctionBetween.apply_closed393    with equatorAntipode.function, real394  have vectorP := S².function with pointIn395  have vectorA := S².function with antipodeIn396  have opposite := equatorAntipode.opposite at t397  have coordinates := matrixVector.opposite at σ, equatorPoint(t),398    equatorAntipode(t) with matrix, vectorP, vectorA, opposite399  have image := matrixVector.vector at σ, equatorAntipode(t)400    with matrix, vectorA401  have row := row3.function at (0:R), (0:R), -(1:R)402  apply FunctionBetween.ext with image, row403  intros i hi404  have coordinate := coordinates with i, hi405  rw [coordinate, pole]406  have alternatives := index.cases with hi407  rcases alternatives with at0 | at1 | at2408  . have other := basis.other at 0, 2409      with index.zero_mem, index.two_mem, index.zero_ne_two410    rw [at0, other, row3.zero]411    ring412  . have other := basis.other at 1, 2413      with index.one_mem, index.two_mem, index.one_ne_two414    rw [at1, other, row3.one]415    ring416  . have same := basis.same at 2 with index.two_mem417    rw [at2, same, row3.two]418    rfl419420theorem actImage.off_axis (σ D t : Set)421  requires rotation : σ ∈ so3Matrices422  requires subset : D ⊆ S²423  requires real : t ∈ ℝ424  requires pole : σ · equatorPoint(t) = basis(2)425  requires offPoint : ¬(equatorPoint(t) ∈ D)426  requires offAntipode : ¬(equatorAntipode(t) ∈ D)427  shows ∀ y ∈ actImage(sphereAction, σ, D), vectorPoint(y) ≠ complexZero428proof429  intros y hy axis430  obtain ⟨d, hd, moved⟩ := actImage.membership.forward with hy431  have dIn := subset with d, hd432  have applied := sphereAction.apply with rotation, dIn433  rw applied at moved434  have vectorD := S².function with dIn435  obtain ⟨sphereSubset, closed⟩ := Invariant.sphere436  have yIn : y ∈ S²437    rw ← moved438    exact closed with σ, rotation, d, dIn439  have poles := sphere.axis_cases with yIn, axis440  have back := matrixVector.transpose_cancel with rotation, vectorD441  rw moved at back442  have pointIn := FunctionBetween.apply_closed with equatorPoint.function, real443  have antipodeIn := FunctionBetween.apply_closed444    with equatorAntipode.function, real445  have vectorP := S².function with pointIn446  have vectorA := S².function with antipodeIn447  cases poles with north | south448  . have backP := matrixVector.transpose_cancel with rotation, vectorP449    rw [pole, basis.two] at backP450    rw north at back451    apply offPoint452    rw [← backP, back]453    exact hd454  . have backA := matrixVector.transpose_cancel with rotation, vectorA455    have antipode := equatorAntipode.image with rotation, real, pole456    rw antipode at backA457    rw south at back458    apply offAntipode459    rw [← backA, back]460    exact hd461462-- The separation theorem for every countable subset of the sphere.463theorem sphere.exists_separating_any (D : Set)464  requires countable : Countable(D)465  requires subset : D ⊆ S²466  shows ∃ ρ ∈ Group.carrier(SO3), ∀ n ∈ ℕ,467    Disjoint(actImage(sphereAction, groupPow(SO3, ρ, n + 1), D), D)468proof469  have outside := equator.exists_outside with countable470  obtain ⟨t, real, offPoint, offAntipode⟩ := outside471  have pointIn := FunctionBetween.apply_closed with equatorPoint.function, real472  obtain ⟨σ, rotation, pole⟩ := so3.transitive_pole with pointIn473  have action := sphereAction.action474  have group := SO3.group475  have σIn : σ ∈ Group.carrier(SO3)476    rw SO3.carrierOf477    exact rotation478  have subsetImage : actImage(sphereAction, σ, D) ⊆ S² :=479    actImage.subset at sphereAction, SO3, S², σ, D with action, subset480  have countableImage := actImage.countable with rotation, subset, countable481  have offAxis := actImage.off_axis482    with rotation, subset, real, pole, offPoint, offAntipode483  obtain ⟨τ, turnIn, separated⟩ := sphere.exists_separating484    with countableImage, subsetImage, offAxis485  have τRotation : τ ∈ so3Matrices486    rw ← SO3.carrierOf487    exact turnIn488  have inverseIn : SO3.inv(σ) ∈ Group.carrier(SO3) :=489    Group.inv_mem with group490  have leftIn : SO3.mul(SO3.inv(σ), τ) ∈ Group.carrier(SO3) :=491    Group.mul_mem with group492  have conjugateIn : SO3.mul(SO3.mul(SO3.inv(σ), τ), σ) ∈ SO3.carrier :=493    Group.mul_mem with group494  refine ⟨SO3.mul(SO3.mul(SO3.inv(σ), τ), σ), conjugateIn, ?_⟩495  intros n hn496  have natural := omega.natural with hn497  have apart := separated with n, hn498  have powerIn : groupPow(SO3, τ, n + 1) ∈ Group.carrier(SO3) :=499    Group.pow_mem with group500  have powerRotation : groupPow(SO3, τ, n + 1) ∈ so3Matrices501    rw ← SO3.carrierOf502    exact powerIn503  have powers := so3.pow_conjugate at σ, τ, n + 1 with rotation, τRotation504  have conjugated := actImage.conjugate at σ, groupPow(SO3, τ, n + 1), D505    with rotation, powerRotation, subset506  have movedSubset := actImage.subset at sphereAction, SO3, S²,507    groupPow(SO3, τ, n + 1), actImage(sphereAction, σ, D)508    with action, subsetImage509  have moved := actImage.disjoint at sphereAction, SO3, S², SO3.inv(σ),510    actImage(sphereAction, groupPow(SO3, τ, n + 1),511      actImage(sphereAction, σ, D)),512    actImage(sphereAction, σ, D) with action, movedSubset, subsetImage, apart513  have back := actImage.inv_image at sphereAction, SO3, S², σ, D514    with action, subset515  rw back at moved516  rw [powers, conjugated]517  exact moved518519-- The sphere absorbs every countable subset.520theorem sphere.absorb_any (D : Set)521  requires countable : Countable(D)522  requires subset : D ⊆ S²523  shows Equidecomposable(sphereAction, SO3, S², S², S² ∖ D)524proof525  have separating := sphere.exists_separating_any with countable, subset526  obtain ⟨ρ, rotation, separated⟩ := separating527  exact sphere.absorb with rotation, subset, separated528