-- The order of turn(t): the plane turn by a complex number z, with
-- planeTurnOf(z)ⁿ = planeTurnOf(zⁿ); turn(t) is the plane turn by the point
-- (turnCos(t), turnSin(t)) of the unit circle, so turn(t)ⁿ = 1 forces that
-- point to be an n-th root of unity, of which there are finitely many;
-- hence turn(t) has infinite order for all but countably many t
-- 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.Order
import Turn
import CountableUnion
import Roots

-- Coordinates of a complex number are real.
instance complexCarrier.fst_real (z : Set)
  requires member : z ∈ complexCarrier
  shows fst(z) ∈ ℝ
proof
  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member
  rw [shape, fst.pair]
  exact aReal

instance complexCarrier.snd_real (z : Set)
  requires member : z ∈ complexCarrier
  shows snd(z) ∈ ℝ
proof
  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member
  rw [shape, snd.pair]
  exact bReal

-- The plane turn by a complex number.
def planeTurnOf (z : Set) : Set := planeTurn(fst(z), snd(z))

theorem planeTurnOf.graph (z : Set)
  shows planeTurnOf(z) = planeTurn(fst(z), snd(z))
proof
  simp [planeTurnOf]

theorem planeTurnOf.pair (a b : Real)
  shows planeTurnOf((a, b)) = planeTurn(a, b)
proof
  rw [planeTurnOf.graph, fst.pair, snd.pair]
  rfl

instance planeTurnOf.matrix (z : Set)
  requires member : z ∈ complexCarrier
  shows planeTurnOf(z) : realRing ^ 3 × 3
proof
  have first := complexCarrier.fst_real with member
  have second := complexCarrier.snd_real with member
  rw planeTurnOf.graph
  exact planeTurn.matrix with *

theorem planeTurnOf.one
  shows planeTurnOf(complexOne) = Ring.one(matrixRing(realRing, 3))
proof
  have pair : complexOne = ((1:R), (0:R))
    unfold complexOne
    rfl
  rw [pair, planeTurnOf.pair]
  exact planeTurn.one

theorem planeTurnOf.mul (z w : Set)
  requires memberZ : z ∈ complexCarrier
  requires memberW : w ∈ complexCarrier
  shows matrixMul3(planeTurnOf(z), planeTurnOf(w)) = planeTurnOf(complexMul(z, w))
proof
  obtain ⟨a, aReal, b, bReal, shapeZ⟩ := complexCarrier.cases with memberZ
  obtain ⟨c, cReal, d, dReal, shapeW⟩ := complexCarrier.cases with memberW
  have product := complexMul.pair at a, b, c, d with *
  have difference : a * c - b * d = a * c + -(b * d)
    ring
  rw [shapeZ, shapeW, planeTurnOf.pair, planeTurnOf.pair, product,
    planeTurnOf.pair, planeTurn.mul, difference]
  rfl

theorem planeTurnOf.pow (z : Set) (n : Nat)
  requires member : z ∈ complexCarrier
  shows planeTurnOf(z) ^ n = planeTurnOf(monoidPow(complexMul, complexOne, z, n))
proof
  induction n
  | zero =>
    have matrix := planeTurnOf.matrix with member
    rw [matrixPow3.zero, monoidPow.zero, planeTurnOf.one]
    rfl
  | succ(k) using ih =>
    have ring := complexes.comm_ring
    have ordinary := IsCommRing.ring with ring
    have monoid := IsRing.multiplicative with ordinary
    have matrix := planeTurnOf.matrix with member
    have power := monoidPow.closed at complexCarrier, complexMul, complexOne, z, k
      with monoid, member
    have succForm : k + 1 = succ(k) := add.right_one at k
    have typed : Matrix3(planeTurnOf(z)) := Matrix3.of_matrix with matrix
    have step := matrixPow3.succ at planeTurnOf(z), k with typed
    rw succForm at step
    have combine := planeTurnOf.mul with member, power
    rw [step, ih, monoidPow.succ]
    exact combine

-- A plane turn equal to the identity is the turn by (1, 0).
theorem planeTurn.eq_one (a b : Real)
  requires same : planeTurn(a, b) = Ring.one(matrixRing(realRing, 3))
  shows a = (1:R) ∧ b = (0:R)
proof
  have comm := realRing.comm_ring
  have zeroIn : 0 ∈ 3 by typecheck
  have oneIn : 1 ∈ 3 by typecheck
  have zeroReal : (0:R) ∈ ℝ by typecheck
  have oneReal : (1:R) ∈ ℝ by typecheck
  have entry00 := matrixRing.one_entry at realRing, 3, 0, 0 with *
  have entry10 := matrixRing.one_entry at realRing, 3, 1, 0 with *
  rw [realRing.carrierOf, realRing.zero_eq, realRing.one_eq] at entry00
  rw [realRing.carrierOf, realRing.zero_eq, realRing.one_eq] at entry10
  have equal : (0:N) = (0:N) by rfl
  have different : (1:N) ≠ (0:N)
    intro flipped
    symm at flipped
    exact threeIndex.zero_ne_one with flipped
  have diagonal := singleValue.same at ℝ, realZero, realOne, 0, 0 with *
  have off := singleValue.other at ℝ, realZero, realOne, 0, 1 with *
  have first := planeTurn.entry00 at a, b
  have second := planeTurn.entry10 at a, b
  constructor
  . calc
      a = planeTurn(a, b)[0, 0] := by rw first
      _ = Ring.one(matrixRing(realRing, 3))[0, 0] := by rw same
      _ = (1:R) := by rw [entry00, diagonal]
  . calc
      b = planeTurn(a, b)[1, 0] := by rw second
      _ = Ring.one(matrixRing(realRing, 3))[1, 0] := by rw same
      _ = (0:R) := by rw [entry10, off]

theorem complexCarrier.eq_one (z : Set)
  requires member : z ∈ complexCarrier
  requires first : fst(z) = (1:R)
  requires second : snd(z) = (0:R)
  shows z = complexOne
proof
  obtain ⟨a, aReal, b, bReal, shape⟩ := complexCarrier.cases with member
  rw [shape, fst.pair] at first
  rw [shape, snd.pair] at second
  rw [shape, first, second]
  unfold complexOne
  rfl

-- The point of the unit circle that turn(t) turns by.
defgraph turnPoint (t ∈ ℝ) : complexCarrier := (turnCos(t), turnSin(t))
proof
  have real : Real(t) by typecheck
  exact complexCarrier.pair at turnCos(t), turnSin(t) with *

theorem turnPoint.injective
  shows InjectiveBetween(turnPoint, ℝ, complexCarrier)
proof
  have function := turnPoint.function
  apply Injective.of_pointwise with function
  intros s hs t ht same
  have valueS := turnPoint.value at s with *
  have valueT := turnPoint.value at t with *
  rw [valueS, valueT] at same
  obtain ⟨cosEqual, sinEqual⟩ := orderedPair.injective with same
  exact turn.injective_of_coordinates with cosEqual, sinEqual

theorem turn.planeTurnOf (t : Real)
  shows turn(t) = planeTurnOf(turnPoint(t))
proof
  have real : t ∈ ℝ by typecheck
  have value := turnPoint.value at t with *
  rw [value, planeTurnOf.pair, turn.graph]
  rfl

-- The parameters t with turn(t)ⁿ = 1, for one n and for some n ≥ 1.
def turnOrderSet (n : Nat) : Set :=
  { t ∈ ℝ | matrixPow3(turn(t), n) = Ring.one(matrixRing(realRing, 3)) }

def turnOrders : Set :=
  { t ∈ ℝ | ∃ n ∈ ℕ, 0 < n ∧ matrixPow3(turn(t), n) = Ring.one(matrixRing(realRing, 3)) }

theorem turnOrderSet.subset (n : Nat)
  shows turnOrderSet(n) ⊆ ℝ
proof
  intros t ht
  have data := turnOrderSet.membership.forward with ht
  exact data.left

-- For n ≥ 1 only finitely many t have turn(t)ⁿ = 1: their points are
-- n-th roots of unity, and t ↦ turnPoint(t) is injective.
theorem turnOrderSet.finite (k : Nat)
  shows Finite(turnOrderSet(k + 1))
proof
  have injective := turnPoint.injective
  have rootsFinite := complexUnityRoots.finite at k
  have preimageFinite := Finite.preimage with injective, rootsFinite
  have bounded : turnOrderSet(k + 1) ⊆ functionPreimage(turnPoint, ℝ, complexUnityRoots(k))
    intros t ht
    obtain ⟨real, power⟩ := turnOrderSet.membership.forward with ht
    have typed : Real(t) by typecheck
    have pointIn : turnPoint(t) ∈ complexCarrier :=
      FunctionBetween.apply_closed with turnPoint.function, real
    have shape := turn.planeTurnOf at t
    have matrixPower := planeTurnOf.pow at turnPoint(t), k + 1 with pointIn
    have succForm : k + 1 = succ(k) := add.right_one at k
    rw shape at power
    have unitPower : planeTurnOf(monoidPow(complexMul, complexOne, turnPoint(t), k + 1)) =
        Ring.one(matrixRing(realRing, 3))
      rw ← matrixPower
      exact power
    have ring := complexes.comm_ring
    have ordinary := IsCommRing.ring with ring
    have monoid := IsRing.multiplicative with ordinary
    have powerIn := monoidPow.closed at complexCarrier, complexMul, complexOne,
      turnPoint(t), k + 1 with monoid, pointIn
    have first := complexCarrier.fst_real with powerIn
    have second := complexCarrier.snd_real with powerIn
    rw planeTurnOf.graph at unitPower
    obtain ⟨fstOne, sndZero⟩ := planeTurn.eq_one with unitPower
    have rootOfUnity := complexCarrier.eq_one with powerIn, fstOne, sndZero
    rw succForm at rootOfUnity
    have inRoots := complexUnityRoots.contains with pointIn, rootOfUnity
    exact functionPreimage.membership.backward with ⟨real, inRoots⟩
  exact Finite.subset with preimageFinite, bounded

-- The family n ↦ turnOrderSet(n + 1), indexed by ℕ.
defgraph turnOrderFamily (n ∈ ℕ) : 𝒫(ℝ) := turnOrderSet(n + 1)
proof
  have subset := turnOrderSet.subset at n + 1
  exact powerset.membership_iff.backward with subset

-- turn(t) has infinite order for all but countably many t.
theorem turn.infinite_order
  shows Countable(turnOrders)
proof
  have function := turnOrderFamily.function
  have naturals := naturals.countable
  have members : ∀ n ∈ ℕ, Countable(turnOrderFamily(n))
    intros n hn
    have natural := omega.natural with hn
    have value := turnOrderFamily.value at n with *
    have finite := turnOrderSet.finite at n
    rw value
    exact Countable.of_finite with finite
  have unionCountable := Countable.indexed_union with function, naturals, members
  have bounded : turnOrders ⊆ ⋃(functionImage(turnOrderFamily, ℕ, 𝒫(ℝ)))
    intros t ht
    obtain ⟨real, n, hn, positive, power⟩ := turnOrders.membership.forward with ht
    have natural := omega.natural with hn
    have alternatives := natural.zero_or_successor at n with natural
    cases alternatives with zero | successor
    . exfalso
      rw zero at positive
      exact Less.irreflexive with positive
    . obtain ⟨k, naturalK, shape⟩ := successor
      have succForm : k + 1 = succ(k) := add.right_one at k
      have kIn : k ∈ ℕ by typecheck
      have value := turnOrderFamily.value at k with *
      have inSet : t ∈ turnOrderSet(k + 1)
        apply turnOrderSet.membership.backward
        refine ⟨real, ?_⟩
        rw [succForm, ← shape]
        exact power
      have familyMember : turnOrderFamily(k) ∈ functionImage(turnOrderFamily, ℕ, 𝒫(ℝ)) :=
        functionImage.value with function, kIn
      rw value at familyMember
      exact union.contains with familyMember, inSet
  exact Countable.subset with unionCountable, bounded