-- turn(t) is a rotation: a plane turn by a point of the unit circle is
-- orthogonal with determinant one, so it lies in SO3
-- 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.TurnRotation
import Turn
import Rotation.Orthogonal

-- The transpose of a plane turn is the turn by the conjugate point.
theorem planeTurn.transposed (a b : Real)
  shows transpose(planeTurn(a, b)) = planeTurn(a, -b)
proof
  have matrix := planeTurn.matrix at a, b
  have matrixT : transpose(planeTurn(a, b)) : realRing ^ 3 × 3 := transpose.matrix with *
  have entries : ∀ i ∈ 3, ∀ j ∈ 3,
      transpose(planeTurn(a, b))[i, j] = planeTurn(a, -b)[i, j]
    intros i hi j hj
    have flip := transpose.entry at planeTurn(a, b), i, j with *
    rw [flip, planeTurn.graph, planeTurn.graph]
    have rows := threeIndex.cases with hi
    have columns := threeIndex.cases with hj
    rcases rows with rowZero | rowOne | rowTwo
    . rcases columns with columnZero | columnOne | columnTwo
      . rw [rowZero, columnZero]
        matrix3of_entries
      . rw [rowZero, columnOne]
        matrix3of_entries
        ring
      . rw [rowZero, columnTwo]
        matrix3of_entries
    . rcases columns with columnZero | columnOne | columnTwo
      . rw [rowOne, columnZero]
        matrix3of_entries
      . rw [rowOne, columnOne]
        matrix3of_entries
      . rw [rowOne, columnTwo]
        matrix3of_entries
    . rcases columns with columnZero | columnOne | columnTwo
      . rw [rowTwo, columnZero]
        matrix3of_entries
      . rw [rowTwo, columnOne]
        matrix3of_entries
      . rw [rowTwo, columnTwo]
        matrix3of_entries
  have negReal : -b ∈ ℝ by typecheck
  have conjugateMatrix : planeTurn(a, -b) : realRing ^ 3 × 3 := planeTurn.matrix with *
  have leftTyped : Matrix3(transpose(planeTurn(a, b))) := Matrix3.of_matrix with matrixT
  have rightTyped : Matrix3(planeTurn(a, -b)) := Matrix3.of_matrix with conjugateMatrix
  exact Matrix3.ext with leftTyped, rightTyped, entries

-- A plane turn by a point of the unit circle is in SO3.
theorem planeTurn.so3 (a b : Real)
  requires circle : a * a + b * b = 1
  shows planeTurn(a, b) ∈ so3Matrices
proof
  have matrix := planeTurn.matrix at a, b
  have transposed := planeTurn.transposed at a, b
  have first : a * a - b * (-b) = (1:R)
    rw ← circle
    ring
  have second : a * (-b) + b * a = (0:R)
    ring
  have third : a * a - (-b) * b = (1:R)
    rw ← circle
    ring
  have fourth : a * b + (-b) * a = (0:R)
    ring
  have right : call2(Ring.mul(matrixRing(realRing, 3)), planeTurn(a, b),
      transpose(planeTurn(a, b))) = Ring.one(matrixRing(realRing, 3))
    rw [← matrixMul3.graph, transposed, planeTurn.mul, first, second]
    exact planeTurn.one
  have left : call2(Ring.mul(matrixRing(realRing, 3)), transpose(planeTurn(a, b)),
      planeTurn(a, b)) = Ring.one(matrixRing(realRing, 3))
    rw [← matrixMul3.graph, transposed, planeTurn.mul, third, fourth]
    exact planeTurn.one
  have orthogonal := Orthogonal.mk with left, right
  have key : determinant3(planeTurn(a, b)) = a * a + b * b
    rw [determinant3.value, planeTurn.graph]
    matrix3of_entries
    ring
  have unit : determinant3(planeTurn(a, b)) = (1:R)
    rw key
    exact circle
  exact so3Matrices.mk with orthogonal, unit

-- turn(t) is a rotation.
theorem turn.rotation (t : Real)
  shows turn(t) ∈ so3Matrices
proof
  have circle := turn.circle at t
  rw turn.graph
  exact planeTurn.so3 with circle

theorem turn.so3 (t : Real)
  shows turn(t) ∈ Group.carrier(SO3)
proof
  rw SO3.carrierOf
  exact turn.rotation at t