Grace/Cumulus/Geometry/Absorption/TurnRotation.g17

Open in Workbench Download source

Imports

Turn · Rotation.Orthogonal

Declarations

• planeTurn.transposed theorem derivation
• planeTurn.so3 theorem derivation
• turn.rotation theorem derivation
• turn.so3 theorem derivation

Source

1-- turn(t) is a rotation: a plane turn by a point of the unit circle is2-- orthogonal with determinant one, so it lies in SO33-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Geometry.Absorption.TurnRotation9import Turn10import Rotation.Orthogonal1112-- The transpose of a plane turn is the turn by the conjugate point.13theorem planeTurn.transposed (a b : Real)14  shows transpose(planeTurn(a, b)) = planeTurn(a, -b)15proof16  have matrix := planeTurn.matrix at a, b17  have matrixT : transpose(planeTurn(a, b)) : realRing ^ 3 × 3 := transpose.matrix with *18  have entries : ∀ i ∈ 3, ∀ j ∈ 3,19      transpose(planeTurn(a, b))[i, j] = planeTurn(a, -b)[i, j]20    intros i hi j hj21    have flip := transpose.entry at planeTurn(a, b), i, j with *22    rw [flip, planeTurn.graph, planeTurn.graph]23    have rows := threeIndex.cases with hi24    have columns := threeIndex.cases with hj25    rcases rows with rowZero | rowOne | rowTwo26    . rcases columns with columnZero | columnOne | columnTwo27      . rw [rowZero, columnZero]28        matrix3of_entries29      . rw [rowZero, columnOne]30        matrix3of_entries31        ring32      . rw [rowZero, columnTwo]33        matrix3of_entries34    . rcases columns with columnZero | columnOne | columnTwo35      . rw [rowOne, columnZero]36        matrix3of_entries37      . rw [rowOne, columnOne]38        matrix3of_entries39      . rw [rowOne, columnTwo]40        matrix3of_entries41    . rcases columns with columnZero | columnOne | columnTwo42      . rw [rowTwo, columnZero]43        matrix3of_entries44      . rw [rowTwo, columnOne]45        matrix3of_entries46      . rw [rowTwo, columnTwo]47        matrix3of_entries48  have negReal : -b ∈ ℝ by typecheck49  have conjugateMatrix : planeTurn(a, -b) : realRing ^ 3 × 3 := planeTurn.matrix with *50  have leftTyped : Matrix3(transpose(planeTurn(a, b))) := Matrix3.of_matrix with matrixT51  have rightTyped : Matrix3(planeTurn(a, -b)) := Matrix3.of_matrix with conjugateMatrix52  exact Matrix3.ext with leftTyped, rightTyped, entries5354-- A plane turn by a point of the unit circle is in SO3.55theorem planeTurn.so3 (a b : Real)56  requires circle : a * a + b * b = 157  shows planeTurn(a, b) ∈ so3Matrices58proof59  have matrix := planeTurn.matrix at a, b60  have transposed := planeTurn.transposed at a, b61  have first : a * a - b * (-b) = (1:R)62    rw ← circle63    ring64  have second : a * (-b) + b * a = (0:R)65    ring66  have third : a * a - (-b) * b = (1:R)67    rw ← circle68    ring69  have fourth : a * b + (-b) * a = (0:R)70    ring71  have right : call2(Ring.mul(matrixRing(realRing, 3)), planeTurn(a, b),72      transpose(planeTurn(a, b))) = Ring.one(matrixRing(realRing, 3))73    rw [← matrixMul3.graph, transposed, planeTurn.mul, first, second]74    exact planeTurn.one75  have left : call2(Ring.mul(matrixRing(realRing, 3)), transpose(planeTurn(a, b)),76      planeTurn(a, b)) = Ring.one(matrixRing(realRing, 3))77    rw [← matrixMul3.graph, transposed, planeTurn.mul, third, fourth]78    exact planeTurn.one79  have orthogonal := Orthogonal.mk with left, right80  have key : determinant3(planeTurn(a, b)) = a * a + b * b81    rw [determinant3.value, planeTurn.graph]82    matrix3of_entries83    ring84  have unit : determinant3(planeTurn(a, b)) = (1:R)85    rw key86    exact circle87  exact so3Matrices.mk with orthogonal, unit8889-- turn(t) is a rotation.90theorem turn.rotation (t : Real)91  shows turn(t) ∈ so3Matrices92proof93  have circle := turn.circle at t94  rw turn.graph95  exact planeTurn.so3 with circle9697theorem turn.so3 (t : Real)98  shows turn(t) ∈ Group.carrier(SO3)99proof100  rw SO3.carrierOf101  exact turn.rotation at t102