-- Separating a countable set from itself by a turn about the z-axis: for
-- a countable D ⊆ S² off the z-axis, all but countably many t have
-- turn(t)ⁿ(D) ∩ D = ∅ for every n ≥ 1, because turn(t)ⁿ · d = e forces the
-- point of turn(t) to be an n-th root of a complex number determined by
-- d and e, and the reals are uncountable
-- 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.Separation
import Order
import TurnRotation
import Real.Uncountable

-- The complex point (v(0), v(1)) of a vector of ℝ³.
def vectorPoint (v : Set) : Set := (v(0), v(1))

theorem vectorPoint.graph (v : Set)
  shows vectorPoint(v) = (v(0), v(1))
proof
  simp [vectorPoint]

theorem vectorPoint.complex (v : Set)
  requires vector : v : 3 → ℝ
  shows vectorPoint(v) ∈ complexCarrier
proof
  have zeroIn : 0 ∈ 3 by typecheck
  have oneIn : 1 ∈ 3 by typecheck
  have first := FunctionBetween.apply_closed with vector, zeroIn
  have second := FunctionBetween.apply_closed with vector, oneIn
  rw vectorPoint.graph
  exact complexCarrier.pair at v(0), v(1) with *

-- The remaining entries of a plane turn.
theorem planeTurn.entry01 (a b : Real)
  shows planeTurn(a, b)[0, 1] = -b
proof
  rw [planeTurn.graph, matrix3of.entry01]
  rfl

theorem planeTurn.entry02 (a b : Real)
  shows planeTurn(a, b)[0, 2] = (0:R)
proof
  rw [planeTurn.graph, matrix3of.entry02]
  rfl

theorem planeTurn.entry11 (a b : Real)
  shows planeTurn(a, b)[1, 1] = a
proof
  rw [planeTurn.graph, matrix3of.entry11]
  rfl

theorem planeTurn.entry12 (a b : Real)
  shows planeTurn(a, b)[1, 2] = (0:R)
proof
  rw [planeTurn.graph, matrix3of.entry12]
  rfl

-- A plane turn acts on the complex point of a vector by multiplication.
theorem planeTurnOf.vector_point (z v : Set)
  requires member : z ∈ complexCarrier
  requires vector : v : 3 → ℝ
  shows vectorPoint(planeTurnOf(z) · v) = complexMul(z, vectorPoint(v))
proof
  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member
  have zeroIn : 0 ∈ 3 by typecheck
  have oneIn : 1 ∈ 3 by typecheck
  have twoIn : 2 ∈ 3 by typecheck
  have v0 := FunctionBetween.apply_closed with vector, zeroIn
  have v1 := FunctionBetween.apply_closed with vector, oneIn
  have v2 := FunctionBetween.apply_closed with vector, twoIn
  have matrix : planeTurn(a, b) : realRing ^ 3 × 3 := planeTurn.matrix with *
  have first := matrixVector.entry at planeTurn(a, b), v, 0 with *
  have second := matrixVector.entry at planeTurn(a, b), v, 1 with *
  rw [planeTurn.entry00, planeTurn.entry01, planeTurn.entry02] at first
  rw [planeTurn.entry10, planeTurn.entry11, planeTurn.entry12] at second
  have product := complexMul.pair at a, b, v(0), v(1) with *
  have horizontal : a * (v(0):R) + (-b) * (v(1):R) + (0:R) * (v(2):R) =
      a * (v(0):R) + -(b * (v(1):R))
    ring
  have vertical : b * (v(0):R) + a * (v(1):R) + (0:R) * (v(2):R) =
      a * (v(1):R) + b * (v(0):R)
    ring
  rw [shape, planeTurnOf.pair, vectorPoint.graph, vectorPoint.graph, product,
    first, second, horizontal, vertical]
  rfl

-- The parameters t with turn(t)ⁿ · d = e.
def turnBad (n : Nat, d e : Set) : Set :=
  { t ∈ ℝ | matrixPow3(turn(t), n) · d = e }

theorem turnBad.subset (n : Nat) (d e : Set)
  shows turnBad(n, d, e) ⊆ ℝ
proof
  intros t ht
  have data := turnBad.membership.forward with ht
  exact data.left

section Complexes
notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)

-- Solving W · p = r when p has the inverse q.
theorem complex.solve_left (W p q r : Set)
  requires wIn : W ∈ complexCarrier
  requires pIn : p ∈ complexCarrier
  requires qIn : q ∈ complexCarrier
  requires rIn : r ∈ complexCarrier
  requires inverse : complexMul(p, q) = complexOne
  requires equation : complexMul(W, p) = r
  shows W = complexMul(r, q)
proof
  have ring := complexes.comm_ring
  have unit : ℂ[W * (p * q)] = W
    rw inverse
    ring
  have regroup : ℂ[W * (p * q)] = ℂ[(W * p) * q]
    ring
  rw [← unit, regroup, equation]
  rfl

end Complexes

-- For n ≥ 1 and d off the z-axis, finitely many t have turn(t)ⁿ · d = e.
theorem turnBad.finite (k : Nat) (d e : Set)
  requires vectorD : d : 3 → ℝ
  requires vectorE : e : 3 → ℝ
  requires offAxis : vectorPoint(d) ≠ complexZero
  shows Finite(turnBad(k + 1, d, e))
proof
  have field := complexes.is_field
  have ring := complexes.comm_ring
  have ordinary := IsCommRing.ring with ring
  have monoid := IsRing.multiplicative with ordinary
  have pointD := vectorPoint.complex at d with vectorD
  have pointE := vectorPoint.complex at e with vectorE
  obtain ⟨commRing, nontrivial, inverses⟩ := field
  obtain ⟨q, inverse⟩ := inverses with vectorPoint(d), pointD, offAxis
  obtain ⟨pIn, qIn, leftLaw, rightLaw⟩ := inverse
  have targetIn := IsRing.mul_closed with ordinary, pointE, qIn
  have injective := turnPoint.injective
  have rootsFinite := complexPowerRoots.finite at complexMul(vectorPoint(e), q), k
    with targetIn
  have preimageFinite := Finite.preimage with injective, rootsFinite
  have bounded : turnBad(k + 1, d, e) ⊆ functionPreimage(turnPoint, ℝ, complexPowerRoots(complexMul(vectorPoint(e), q), k))
    intros t ht
    obtain ⟨real, moved⟩ := turnBad.membership.forward with ht
    have pointIn : turnPoint(t) ∈ complexCarrier :=
      FunctionBetween.apply_closed with turnPoint.function, real
    have powerIn := monoidPow.closed at complexCarrier, complexMul, complexOne,
      turnPoint(t), k + 1 with monoid, pointIn
    have shape := turn.planeTurnOf at t
    have matrixPower := planeTurnOf.pow at turnPoint(t), k + 1 with pointIn
    rw [shape, matrixPower] at moved
    have law := planeTurnOf.vector_point with powerIn, vectorD
    rw moved at law
    symm at law
    have rootEquation := complex.solve_left with powerIn, pIn, qIn, pointE, rightLaw, law
    have succForm : k + 1 = succ(k) := add.right_one at k
    rw succForm at rootEquation
    have inRoots := complexPowerRoots.contains with pointIn, targetIn, rootEquation
    exact functionPreimage.membership.backward with ⟨real, inRoots⟩
  exact Finite.subset with preimageFinite, bounded

-- The family of these sets over the indices (n, (d, e)), and their union.
defgraph turnBadFamily (D : Set) (p ∈ ℕ × (D × D)) : 𝒫(ℝ) :=
  turnBad(succ(fst(p)), fst(snd(p)), snd(snd(p)))
proof
  obtain ⟨bound, n, hn, q, hq, shape⟩ := product.membership.forward with member
  have natural := omega.natural with hn
  have natSucc : Nat(succ(n)) by typecheck
  rw [shape, fst.pair, snd.pair]
  have subset := turnBad.subset at succ(n), fst(q), snd(q) with natSucc
  exact powerset.membership_iff.backward with subset

def turnBadSet (D : Set) : Set :=
  ⋃(functionImage(turnBadFamily(D), ℕ × (D × D), 𝒫(ℝ)))

theorem turnBadSet.graph (D : Set)
  shows turnBadSet(D) = ⋃(functionImage(turnBadFamily(D), ℕ × (D × D), 𝒫(ℝ)))
proof
  simp [turnBadSet]

theorem turnBadSet.contains (D t : Set) (n : Nat) (d e : Set)
  requires hd : d ∈ D
  requires he : e ∈ D
  requires member : t ∈ turnBad(n + 1, d, e)
  shows t ∈ turnBadSet(D)
proof
  have function := turnBadFamily.function at D
  have pairIn := product.pair at d, e, D, D with *
  have nIn : n ∈ ℕ by typecheck
  have indexIn := product.pair at n, (d, e), ℕ, D × D with *
  have value := turnBadFamily.value at D, (n, (d, e)) with *
  have succForm : n + 1 = succ(n) := add.right_one at n
  rw [fst.pair, snd.pair, fst.pair, snd.pair] at value
  have familyMember : turnBadFamily(D)((n, (d, e))) ∈ functionImage(turnBadFamily(D), ℕ × (D × D), 𝒫(ℝ)) :=
    functionImage.value with function, indexIn
  rw value at familyMember
  rw succForm at member
  rw turnBadSet.graph
  exact union.contains with familyMember, member

theorem turnBadSet.countable (D : Set)
  requires countable : Countable(D)
  requires subset : D ⊆ S²
  requires offAxis : ∀ d ∈ D, vectorPoint(d) ≠ complexZero
  shows Countable(turnBadSet(D))
proof
  have function := turnBadFamily.function at D
  have pairs := Countable.product with countable, countable
  have index := Countable.product with naturals.countable, pairs
  have members : ∀ p ∈ ℕ × (D × D), Countable(turnBadFamily(D)(p))
    intros p hp
    obtain ⟨bound, n, hn, q, hq, shape⟩ := product.membership.forward with hp
    obtain ⟨boundQ, d, hd, e, he, shapeQ⟩ := product.membership.forward with hq
    have natural := omega.natural with hn
    have value := turnBadFamily.value at D, p with *
    rw [value, shape, shapeQ, fst.pair, snd.pair, fst.pair, snd.pair]
    have vectorD := S².function with (subset with d, hd)
    have vectorE := S².function with (subset with e, he)
    have away := offAxis with d, hd
    have finite := turnBad.finite at n, d, e with vectorD, vectorE, away
    have succForm : n + 1 = succ(n) := add.right_one at n
    rw succForm at finite
    exact Countable.of_finite with finite
  rw turnBadSet.graph
  exact Countable.indexed_union with function, index, members

-- Some real parameter lies outside the countable bad set.
theorem turnBadSet.exists_outside (D : Set)
  requires countable : Countable(D)
  requires subset : D ⊆ S²
  requires offAxis : ∀ d ∈ D, vectorPoint(d) ≠ complexZero
  shows ∃ t ∈ ℝ, ¬(t ∈ turnBadSet(D))
proof
  have badCountable := turnBadSet.countable with countable, subset, offAxis
  have uncountable := reals.uncountable
  unfold Uncountable at uncountable
  by_contra
  rename this => none
  have cover : ℝ ⊆ turnBadSet(D)
    intros t ht
    by_contra
    apply none
    exact ⟨t, ht, this⟩
  have realsCountable := Countable.subset with badCountable, cover
  exact uncountable with realsCountable