-- The absorption tool on the sphere: for a countable D ⊆ S² off the
-- z-axis some turn(t) carries every positive power of D off D, so that D
-- is absorbed into S² by the rotation group
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Geometry.Absorption.Sphere
import Separation
import Absorb

-- Powers of turn(t) in the group SO3 are its matrix powers.
theorem turn.groupPow (t : Real) (n : Nat)
  shows groupPow(SO3, turn(t), n) = matrixPow3(turn(t), n)
proof
  induction n
  | zero =>
    have group := SO3.group
    have rotation := turn.so3 at t
    have unit : groupPow(SO3, turn(t), 0) = Group.one(SO3) := pow_zero with group, rotation
    rw [unit, SO3.oneOf, matrixPow3.zero]
    rfl
  | succ(k) using ih =>
    have group := SO3.group
    have rotation := turn.so3 at t
    have rotationIn : turn(t) ∈ so3Matrices := turn.rotation at t
    have step := pow_succ_left at SO3, turn(t), k with group
    have succForm : k + 1 = succ(k) := add.right_one at k
    rw succForm at step
    have powerIn : groupPow(SO3, turn(t), k) ∈ Group.carrier(SO3) :=
      Group.pow_mem with *
    rw SO3.carrierOf at powerIn
    have ring := matrixRing.real_ring
    have magma := IsSemigroup.magma with
      (IsMonoid.semigroup with (IsRing.multiplicative with (Ring.parts with ring)))
    have carrierSubset : so3Matrices ⊆ Ring.carrier(matrixRing(realRing, 3))
      intros M hM
      obtain ⟨inRing, orthogonal, unit⟩ := so3Matrices.membership.forward with hM
      exact inRing
    have closedMul : ClosedBinary(so3Matrices, Ring.mul(matrixRing(realRing, 3)))
      intros M hM N hN
      have matrixM := so3Matrices.matrix with hM
      have matrixN := so3Matrices.matrix with hN
      exact so3Matrices.mul_mem with *
    have operation := restrictBinary.value at Ring.carrier(matrixRing(realRing, 3)),
      so3Matrices, Ring.mul(matrixRing(realRing, 3)), turn(t), groupPow(SO3, turn(t), k)
      with magma, carrierSubset, closedMul, rotationIn, powerIn
    have matrixStep := matrixPow3.succ at turn(t), k
    rw succForm at matrixStep
    rw [step, SO3.mulOf, operation, ih, matrixStep, matrixMul3.graph]
    rfl

-- The separation theorem for the z-axis: for a countable D ⊆ S² off the
-- axis, some turn(t) carries every positive power of D off D.
theorem turn.separates (D : Set)
  requires countable : Countable(D)
  requires subset : D ⊆ S²
  requires offAxis : ∀ d ∈ D, vectorPoint(d) ≠ complexZero
  shows ∃ t ∈ ℝ, ∀ n ∈ ℕ,
    Disjoint(actImage(sphereAction, groupPow(SO3, turn(t), n + 1), D), D)
proof
  obtain ⟨t, real, outside⟩ := turnBadSet.exists_outside with countable, subset, offAxis
  have typed : Real(t) by typecheck
  refine ⟨t, real, ?_⟩
  intros n hn
  have natural := omega.natural with hn
  have group := SO3.group
  have rotation := turn.so3 at t
  apply Disjoint.iff.backward
  intros y hy inD
  obtain ⟨d, hd, moved⟩ := actImage.membership.forward with hy
  have powerIn : groupPow(SO3, turn(t), n + 1) ∈ Group.carrier(SO3) :=
    Group.pow_mem with *
  rw SO3.carrierOf at powerIn
  have dIn := subset with d, hd
  have applied := sphereAction.apply with powerIn, dIn
  have bridge := turn.groupPow at t, n + 1
  rw [applied, bridge] at moved
  have bad : t ∈ turnBad(n + 1, d, y)
    apply turnBad.membership.backward
    exact ⟨real, moved⟩
  have inBadSet := turnBadSet.contains with hd, inD, bad
  exact outside with inBadSet