-- The points of the sphere fixed by some nontrivial reduced word form a
-- countable set, coded through the pairing of ℕ × ℕ
-- 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.Hausdorff.Countable
import Hom
import FixedPoints
import Geometry.Absorption.CountableUnion

-- The points of the sphere fixed by the rotation of some nontrivial
-- reduced word.
def wordFixedSet : Set :=
  { v ∈ S² | ∃ w ∈ reducedWords,
    w ≠ [] ∧ call2(sphereAction, wordRotation(w), v) = v }

theorem wordFixedSet.subset
  shows wordFixedSet ⊆ S²
proof
  intros v hv
  have parts := wordFixedSet.membership.forward with hv
  exact parts.left

-- Coding words by naturals: the empty word is 0, and a letter in front
-- is paired with the code of the rest.
def wordCode (w : List(4)) → Set
  | [] => 0
  | x :: xs => succ(naturalPairing((x, wordCode(xs))))

theorem wordCode.nil
  shows wordCode([]) = 0
proof
  simp [wordCode]

theorem wordCode.cons (x : Set) (xs : List(4))
  requires hx : x ∈ 4
  shows wordCode(x :: xs) = succ(naturalPairing((x, wordCode(xs))))
proof
  simp [wordCode]

theorem wordCode.natural (w : List(4))
  shows wordCode(w) ∈ ℕ
proof
  induction w
  | List.nil =>
    rw wordCode.nil
    typecheck
  | List.cons(x, xs) using ih =>
    have hx : x ∈ 4 by assumption
    have natural := letter.natural with hx
    have xIn : x ∈ ℕ := nat.omega.forward with natural
    have pair := product.pair at x, wordCode(xs), ℕ, ℕ with xIn, ih
    have function := naturalPairing.function
    have codeIn := FunctionBetween.apply_closed with function, pair
    have head := wordCode.cons at x, xs with hx
    rw head
    exact omega.successor with codeIn

theorem wordCode.injective (u : List(4))
  shows ∀ v, List(4, v) → wordCode(u) = wordCode(v) → u = v
proof
  induction u
  | List.nil =>
    intros v listV same
    have shape := List.cases at 4, v with listV
    cases shape with nil | cons
    . rw nil
      rfl
    . obtain ⟨y, hy, ys, tailList, equal⟩ := cons
      exfalso
      have headY := wordCode.cons at y, ys with hy
      rw [equal, headY, wordCode.nil] at same
      exact Naturals.disjoint.zero.succ at naturalPairing((y, wordCode(ys)))
        with same
  | List.cons(x, xs) using ih =>
    intros v listV same
    have hx : x ∈ 4 by assumption
    have headX := wordCode.cons at x, xs with hx
    have shape := List.cases at 4, v with listV
    cases shape with nil | cons
    . exfalso
      rw [nil, headX, wordCode.nil] at same
      symm at same
      exact Naturals.disjoint.zero.succ at naturalPairing((x, wordCode(xs)))
        with same
    . obtain ⟨y, hy, ys, tailList, equal⟩ := cons
      have headY := wordCode.cons at y, ys with hy
      rw [equal, headX, headY] at same
      have codes := Naturals.injective.succ with same
      have naturalX := nat.omega.forward with (letter.natural with hx)
      have naturalY := nat.omega.forward with (letter.natural with hy)
      have codeX := wordCode.natural at xs with *
      have codeY := wordCode.natural at ys with *
      have pairX := product.pair at x, wordCode(xs), ℕ, ℕ with naturalX, codeX
      have pairY := product.pair at y, wordCode(ys), ℕ, ℕ with naturalY, codeY
      have injective := naturalPairing.injective
      have pairs := Injective.apply_cancel with injective, pairX, pairY, codes
      obtain ⟨sameHead, sameCode⟩ := orderedPair.injective with pairs
      have sameTail := ih with ys, tailList, sameCode
      rw [equal, sameHead, sameTail]
      rfl

-- The code as a graph on the reduced words, so the reduced words are
-- countable.
defgraph wordIndex (w ∈ reducedWords) : ℕ := wordCode(w)
proof
  have list := reducedWords.list with member
  exact wordCode.natural with list

theorem reducedWords.countable
  shows Countable(reducedWords)
proof
  have function := wordIndex.function
  witness wordIndex
  apply Injective.of_pointwise with function
  intros a ha b hb same
  have listA := reducedWords.list with ha
  have listB := reducedWords.list with hb
  have valueA := wordIndex.value with ha
  have valueB := wordIndex.value with hb
  rw [valueA, valueB] at same
  have cancel := wordCode.injective at a with listA
  exact cancel with listB, same

-- The points fixed by the rotation of one word, empty for the empty word.
def fixedBy (w : Set) : Set :=
  { v ∈ S² | w ≠ [] ∧ call2(sphereAction, wordRotation(w), v) = v }

theorem fixedBy.subset (w : Set)
  shows fixedBy(w) ⊆ S²
proof
  intros v hv
  have parts := fixedBy.membership.forward with hv
  exact parts.left

-- A nontrivial word fixes at most a point and its opposite.
theorem fixedBy.countable (w : Set)
  requires hw : w ∈ reducedWords
  shows Countable(fixedBy(w))
proof
  have split : w = [] ∨ w ≠ [] by tauto
  cases split with empty | nonempty
  . have finiteEmpty := Finite.empty
    have countableEmpty := Countable.of_finite with finiteEmpty
    have subset : fixedBy(w) ⊆ ∅
      intros v hv
      obtain ⟨vIn, nonempty, fixed⟩ := fixedBy.membership.forward with hv
      exfalso
      exact nonempty with empty
    exact Countable.subset with countableEmpty, subset
  . have list := reducedWords.list with hw
    have reduced := reducedWords.reduced with hw
    have rotation := wordRotation.so3 with list
    have nontrivial := wordRotation.ne_one with list, reduced, nonempty
    obtain ⟨p, hp, bound⟩ := so3.fixed_points with rotation, nontrivial
    have finiteSingle := Finite.singleton at vectorNeg(p)
    have finitePair := Finite.insert at {vectorNeg(p)}, p with finiteSingle
    have countablePair := Countable.of_finite with finitePair
    have subset : fixedBy(w) ⊆ insert(p, {vectorNeg(p)})
      intros v hv
      obtain ⟨vIn, nonempty2, fixed⟩ := fixedBy.membership.forward with hv
      have applied := sphereAction.apply with rotation, vIn
      rw applied at fixed
      have alternatives := bound with v, vIn, fixed
      apply insert.membership.backward
      cases alternatives with same | opposite
      . left
        exact same
      . right
        rw opposite
        exact singleton.self
    exact Countable.subset with countablePair, subset

-- The fixed sets as a family indexed by the reduced words.
defgraph fixedFamily (w ∈ reducedWords) : 𝒫(S²) := fixedBy(w)
proof
  have subset := fixedBy.subset at w
  exact powerset.membership_iff.backward with subset

theorem wordFixedSet.countable
  shows Countable(wordFixedSet)
proof
  have function := fixedFamily.function
  have countable := reducedWords.countable
  have members : ∀ w ∈ reducedWords, Countable(fixedFamily(w))
    intros w hw
    have value := fixedFamily.value with hw
    rw value
    exact fixedBy.countable with hw
  have union := Countable.indexed_union with function, countable, members
  have subset : wordFixedSet ⊆
      ⋃(functionImage(fixedFamily, reducedWords, 𝒫(S²)))
    intros v hv
    obtain ⟨vIn, w, hw, nonempty, fixed⟩ :=
      wordFixedSet.membership.forward with hv
    have value := fixedFamily.value with hw
    have inFixed : v ∈ fixedBy(w) :=
      fixedBy.membership.backward with ⟨vIn, nonempty, fixed⟩
    have closed := FunctionBetween.apply_closed with function, hw
    have imageIn : fixedFamily(w) ∈ functionImage(fixedFamily,
        reducedWords, 𝒫(S²)) :=
      functionImage.membership.backward with ⟨closed, w, hw, rfl⟩
    rw ← value at inFixed
    exact union.membership.backward with ⟨fixedFamily(w), imageIn, inFixed⟩
  exact Countable.subset with union, subset