Grace/Cumulus/Geometry/Absorption/Final.g17

Open in Workbench Download source

Imports

Sphere · Pieces

Declarations

• sphere.exists_separating theorem derivation
• sphere.absorb_countable theorem derivation

Source

1-- Absorbing a countable set into the sphere: for a countable D ⊆ S² off2-- the z-axis there is a rotation ρ ∈ SO3 with ρⁿ(D) ∩ D = ∅ for every3-- n ≥ 1, and S² and S² ∖ D are SO3-equidecomposable4-- 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.Final10import Sphere11import Pieces1213-- A rotation separating D from its positive powers.14theorem sphere.exists_separating (D : Set)15  requires countable : Countable(D)16  requires subset : D ⊆ S²17  requires offAxis : ∀ d ∈ D, vectorPoint(d) ≠ complexZero18  shows ∃ ρ ∈ Group.carrier(SO3), ∀ n ∈ ℕ,19    Disjoint(actImage(sphereAction, groupPow(SO3, ρ, n + 1), D), D)20proof21  obtain ⟨t, real, separated⟩ := turn.separates with countable, subset, offAxis22  have typed : Real(t) by typecheck23  have rotation := turn.so3 at t24  exact ⟨turn(t), rotation, separated⟩2526-- The sphere absorbs every countable set off the z-axis.27theorem sphere.absorb_countable (D : Set)28  requires countable : Countable(D)29  requires subset : D ⊆ S²30  requires offAxis : ∀ d ∈ D, vectorPoint(d) ≠ complexZero31  shows Equidecomposable(sphereAction, SO3, S², S², S² ∖ D)32proof33  obtain ⟨ρ, rotation, separated⟩ := sphere.exists_separating with countable, subset, offAxis34  exact sphere.absorb with rotation, subset, separated35