Grace/Cumulus/Geometry/Absorption/Sphere.g17

Open in Workbench Download source

Imports

Separation · Absorb

Declarations

• turn.groupPow theorem derivation
• turn.separates theorem derivation

Source

1-- The absorption tool on the sphere: for a countable D ⊆ S² off the2-- z-axis some turn(t) carries every positive power of D off D, so that D3-- is absorbed into S² by the rotation group4-- 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.Absorption.Sphere10import Separation11import Absorb1213-- Powers of turn(t) in the group SO3 are its matrix powers.14theorem turn.groupPow (t : Real) (n : Nat)15  shows groupPow(SO3, turn(t), n) = matrixPow3(turn(t), n)16proof17  induction n18  | zero =>19    have group := SO3.group20    have rotation := turn.so3 at t21    have unit : groupPow(SO3, turn(t), 0) = Group.one(SO3) := pow_zero with group, rotation22    rw [unit, SO3.oneOf, matrixPow3.zero]23    rfl24  | succ(k) using ih =>25    have group := SO3.group26    have rotation := turn.so3 at t27    have rotationIn : turn(t) ∈ so3Matrices := turn.rotation at t28    have step := pow_succ_left at SO3, turn(t), k with group29    have succForm : k + 1 = succ(k) := add.right_one at k30    rw succForm at step31    have powerIn : groupPow(SO3, turn(t), k) ∈ Group.carrier(SO3) :=32      Group.pow_mem with *33    rw SO3.carrierOf at powerIn34    have ring := matrixRing.real_ring35    have magma := IsSemigroup.magma with36      (IsMonoid.semigroup with (IsRing.multiplicative with (Ring.parts with ring)))37    have carrierSubset : so3Matrices ⊆ Ring.carrier(matrixRing(realRing, 3))38      intros M hM39      obtain ⟨inRing, orthogonal, unit⟩ := so3Matrices.membership.forward with hM40      exact inRing41    have closedMul : ClosedBinary(so3Matrices, Ring.mul(matrixRing(realRing, 3)))42      intros M hM N hN43      have matrixM := so3Matrices.matrix with hM44      have matrixN := so3Matrices.matrix with hN45      exact so3Matrices.mul_mem with *46    have operation := restrictBinary.value at Ring.carrier(matrixRing(realRing, 3)),47      so3Matrices, Ring.mul(matrixRing(realRing, 3)), turn(t), groupPow(SO3, turn(t), k)48      with magma, carrierSubset, closedMul, rotationIn, powerIn49    have matrixStep := matrixPow3.succ at turn(t), k50    rw succForm at matrixStep51    rw [step, SO3.mulOf, operation, ih, matrixStep, matrixMul3.graph]52    rfl5354-- The separation theorem for the z-axis: for a countable D ⊆ S² off the55-- axis, some turn(t) carries every positive power of D off D.56theorem turn.separates (D : Set)57  requires countable : Countable(D)58  requires subset : D ⊆ S²59  requires offAxis : ∀ d ∈ D, vectorPoint(d) ≠ complexZero60  shows ∃ t ∈ ℝ, ∀ n ∈ ℕ,61    Disjoint(actImage(sphereAction, groupPow(SO3, turn(t), n + 1), D), D)62proof63  obtain ⟨t, real, outside⟩ := turnBadSet.exists_outside with countable, subset, offAxis64  have typed : Real(t) by typecheck65  refine ⟨t, real, ?_⟩66  intros n hn67  have natural := omega.natural with hn68  have group := SO3.group69  have rotation := turn.so3 at t70  apply Disjoint.iff.backward71  intros y hy inD72  obtain ⟨d, hd, moved⟩ := actImage.membership.forward with hy73  have powerIn : groupPow(SO3, turn(t), n + 1) ∈ Group.carrier(SO3) :=74    Group.pow_mem with *75  rw SO3.carrierOf at powerIn76  have dIn := subset with d, hd77  have applied := sphereAction.apply with powerIn, dIn78  have bridge := turn.groupPow at t, n + 179  rw [applied, bridge] at moved80  have bad : t ∈ turnBad(n + 1, d, y)81    apply turnBad.membership.backward82    exact ⟨real, moved⟩83  have inBadSet := turnBadSet.contains with hd, inD, bad84  exact outside with inBadSet85