Grace/Cumulus/Geometry/Sphere/Transitive.g17

Open in Workbench Download source

Imports

Rotation.Freeness

Declarations

Source

1-- Every point of the unit sphere is carried to the north pole by a2-- rotation, written by coordinates3-- 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.Sphere.Transitive9import Rotation.Freeness1011-- The half turn about the axis through q + e₃ for q = (x, y, z) on the12-- sphere with z ≠ -1 and w = 1 / (1 + z): the matrix13-- w (q + e₃)(q + e₃)ᵀ - 1.14def poleRotation (x y z w : Real) : Set :=15  mat3(x * x * w - 1, x * y * w, x, x * y * w, y * y * w - 1, y, x, y, z)1617-- The half turn about the x-axis.18def flipRotation : Set :=19  mat3((1:R), (0:R), (0:R), (0:R), -(1:R), (0:R), (0:R), (0:R), -(1:R))2021section PoleEntries22variable (x y z w : Real)2324instance poleRotation.matrix25  shows poleRotation(x, y, z, w) : realRing ^ 3 × 326proof27  unfold poleRotation28  exact mat3.matrix with *2930theorem poleRotation.entries31  shows poleRotation(x, y, z, w)[0, 0] = x * x * w - 1 ∧32    poleRotation(x, y, z, w)[0, 1] = x * y * w ∧33    poleRotation(x, y, z, w)[0, 2] = x ∧34    poleRotation(x, y, z, w)[1, 0] = x * y * w ∧35    poleRotation(x, y, z, w)[1, 1] = y * y * w - 1 ∧36    poleRotation(x, y, z, w)[1, 2] = y ∧37    poleRotation(x, y, z, w)[2, 0] = x ∧38    poleRotation(x, y, z, w)[2, 1] = y ∧39    poleRotation(x, y, z, w)[2, 2] = z40proof41  have e00 := mat3.e00 at x * x * w - 1, x * y * w, x, x * y * w, y * y * w - 1,42    y, x, y, z with *43  have e01 := mat3.e01 at x * x * w - 1, x * y * w, x, x * y * w, y * y * w - 1,44    y, x, y, z with *45  have e02 := mat3.e02 at x * x * w - 1, x * y * w, x, x * y * w, y * y * w - 1,46    y, x, y, z with *47  have e10 := mat3.e10 at x * x * w - 1, x * y * w, x, x * y * w, y * y * w - 1,48    y, x, y, z with *49  have e11 := mat3.e11 at x * x * w - 1, x * y * w, x, x * y * w, y * y * w - 1,50    y, x, y, z with *51  have e12 := mat3.e12 at x * x * w - 1, x * y * w, x, x * y * w, y * y * w - 1,52    y, x, y, z with *53  have e20 := mat3.e20 at x * x * w - 1, x * y * w, x, x * y * w, y * y * w - 1,54    y, x, y, z with *55  have e21 := mat3.e21 at x * x * w - 1, x * y * w, x, x * y * w, y * y * w - 1,56    y, x, y, z with *57  have e22 := mat3.e22 at x * x * w - 1, x * y * w, x, x * y * w, y * y * w - 1,58    y, x, y, z with *59  have unfolded : poleRotation(x, y, z, w) =60      mat3(x * x * w - 1, x * y * w, x, x * y * w, y * y * w - 1, y, x, y, z)61    simp [poleRotation]62  rw unfolded63  exact ⟨e00, e01, e02, e10, e11, e12, e20, e21, e22⟩6465-- Under x² + y² + z² = 1 and w (1 + z) = 1 the half turn is special66-- orthogonal: each entry condition is a combination of the two relations.67theorem poleRotation.so368  requires sphere : x * x + y * y + z * z = 169  requires wz : w * (1 + z) = 170  shows poleRotation(x, y, z, w) ∈ so3Matrices71proof72  obtain ⟨e00, e01, e02, e10, e11, e12, e20, e21, e22⟩ :=73    poleRotation.entries at x, y, z, w74  have matrix := poleRotation.matrix at x, y, z, w75  have orthogonal : Orthogonal(poleRotation(x, y, z, w))76    apply Orthogonal.of_entries with matrix77    . rw [e00, e10, e20]78      linear_combination (x * x * w * w) * sphere +79        (x * x * (w * (1 - z) - 1)) * wz80    . rw [e01, e11, e21]81      linear_combination (y * y * w * w) * sphere +82        (y * y * (w * (1 - z) - 1)) * wz83    . rw [e02, e12, e22]84      linear_combination sphere85    . rw [e00, e01, e10, e11, e20, e21]86      linear_combination (x * y * w * w) * sphere +87        (x * y * (w * (1 - z) - 1)) * wz88    . rw [e00, e02, e10, e12, e20, e22]89      linear_combination (x * w) * sphere +90        (x * (1 - z)) * wz91    . rw [e01, e02, e11, e12, e21, e22]92      linear_combination (y * w) * sphere +93        (y * (1 - z)) * wz94    . rw [e00, e01, e02]95      linear_combination (x * x * w * w) * sphere +96        (x * x * (w * (1 - z) - 1)) * wz97    . rw [e10, e11, e12]98      linear_combination (y * y * w * w) * sphere +99        (y * y * (w * (1 - z) - 1)) * wz100    . rw [e20, e21, e22]101      linear_combination sphere102    . rw [e00, e01, e02, e10, e11, e12]103      linear_combination (x * y * w * w) * sphere +104        (x * y * (w * (1 - z) - 1)) * wz105    . rw [e00, e01, e02, e20, e21, e22]106      linear_combination (x * w) * sphere +107        (x * (1 - z)) * wz108    . rw [e10, e11, e12, e20, e21, e22]109      linear_combination (y * w) * sphere +110        (y * (1 - z)) * wz111  have unit : determinant3(poleRotation(x, y, z, w)) = (1:R)112    rw [determinant3.value, e00, e01, e02, e10, e11, e12, e20, e21, e22]113    linear_combination (1 - w * z) * sphere - (z * (1 - z)) * wz114  exact so3Matrices.mk with orthogonal, unit115116end PoleEntries117118-- The half turn carries q to the north pole e₃ = basis(2).119theorem poleRotation.pole (q : Set) (w : Real)120  requires sphere : q ∈ S²121  requires wz : w * ((1:R) + (q(2):R)) = (1:R)122  shows poleRotation(q(0), q(1), q(2), w) · q = basis(2)123proof124  have vector := S².function with sphere125  have q0 := vector.component_real at q, 0 with vector, index.zero_mem126  have q1 := vector.component_real at q, 1 with vector, index.one_mem127  have q2 := vector.component_real at q, 2 with vector, index.two_mem128  obtain ⟨inSpace, unit⟩ := S².membership.forward with sphere129  rw normSq.value at unit130  obtain ⟨e00, e01, e02, e10, e11, e12, e20, e21, e22⟩ :=131    poleRotation.entries at q(0), q(1), q(2), w132  have matrix := poleRotation.matrix at q(0), q(1), q(2), w133  have image := matrixVector.vector at poleRotation(q(0), q(1), q(2), w), q134    with *135  have pole := basis.vector at 2 with index.two_mem136  apply FunctionBetween.ext with image, pole137  intros i hi138  have entry := matrixVector.entry at poleRotation(q(0), q(1), q(2), w), q, i139    with *140  rw entry141  have alternatives := index.cases with hi142  rcases alternatives with at0 | at1 | at2143  . have other := basis.other at 0, 2144      with index.zero_mem, index.two_mem, index.zero_ne_two145    rw [at0, e00, e01, e02, other]146    linear_combination ((q(0):R) * w) * unit +147      ((q(0):R) * (1 - (q(2):R))) * wz148  . have other := basis.other at 1, 2149      with index.one_mem, index.two_mem, index.one_ne_two150    rw [at1, e10, e11, e12, other]151    linear_combination ((q(1):R) * w) * unit +152      ((q(1):R) * (1 - (q(2):R))) * wz153  . have same := basis.same at 2 with index.two_mem154    rw [at2, e20, e21, e22, same]155    linear_combination unit156157-- The half turn about the x-axis.158instance flipRotation.matrix159  shows flipRotation : realRing ^ 3 × 3160proof161  unfold flipRotation162  exact mat3.matrix with *163164theorem flipRotation.entries165  shows flipRotation[0, 0] = (1:R) ∧ flipRotation[0, 1] = (0:R) ∧166    flipRotation[0, 2] = (0:R) ∧ flipRotation[1, 0] = (0:R) ∧167    flipRotation[1, 1] = -(1:R) ∧ flipRotation[1, 2] = (0:R) ∧168    flipRotation[2, 0] = (0:R) ∧ flipRotation[2, 1] = (0:R) ∧169    flipRotation[2, 2] = -(1:R)170proof171  have negOne : -(1:R) ∈ ℝ by typecheck172  have e00 := mat3.e00 at (1:R), (0:R), (0:R), (0:R),173    -(1:R), (0:R), (0:R), (0:R), -(1:R) with *174  have e01 := mat3.e01 at (1:R), (0:R), (0:R), (0:R),175    -(1:R), (0:R), (0:R), (0:R), -(1:R) with *176  have e02 := mat3.e02 at (1:R), (0:R), (0:R), (0:R),177    -(1:R), (0:R), (0:R), (0:R), -(1:R) with *178  have e10 := mat3.e10 at (1:R), (0:R), (0:R), (0:R),179    -(1:R), (0:R), (0:R), (0:R), -(1:R) with *180  have e11 := mat3.e11 at (1:R), (0:R), (0:R), (0:R),181    -(1:R), (0:R), (0:R), (0:R), -(1:R) with *182  have e12 := mat3.e12 at (1:R), (0:R), (0:R), (0:R),183    -(1:R), (0:R), (0:R), (0:R), -(1:R) with *184  have e20 := mat3.e20 at (1:R), (0:R), (0:R), (0:R),185    -(1:R), (0:R), (0:R), (0:R), -(1:R) with *186  have e21 := mat3.e21 at (1:R), (0:R), (0:R), (0:R),187    -(1:R), (0:R), (0:R), (0:R), -(1:R) with *188  have e22 := mat3.e22 at (1:R), (0:R), (0:R), (0:R),189    -(1:R), (0:R), (0:R), (0:R), -(1:R) with *190  have unfolded : flipRotation =191      mat3((1:R), (0:R), (0:R), (0:R), -(1:R), (0:R), (0:R), (0:R), -(1:R))192    simp [flipRotation]193  rw unfolded194  exact ⟨e00, e01, e02, e10, e11, e12, e20, e21, e22⟩195196theorem flipRotation.so3197  shows flipRotation ∈ so3Matrices198proof199  obtain ⟨e00, e01, e02, e10, e11, e12, e20, e21, e22⟩ :=200    flipRotation.entries201  have orthogonal : Orthogonal(flipRotation)202    apply Orthogonal.of_entries with flipRotation.matrix203    . rw [e00, e10, e20]204      ring205    . rw [e01, e11, e21]206      ring207    . rw [e02, e12, e22]208      ring209    . rw [e00, e01, e10, e11, e20, e21]210      ring211    . rw [e00, e02, e10, e12, e20, e22]212      ring213    . rw [e01, e02, e11, e12, e21, e22]214      ring215    . rw [e00, e01, e02]216      ring217    . rw [e10, e11, e12]218      ring219    . rw [e20, e21, e22]220      ring221    . rw [e00, e01, e02, e10, e11, e12]222      ring223    . rw [e00, e01, e02, e20, e21, e22]224      ring225    . rw [e10, e11, e12, e20, e21, e22]226      ring227  have unit : determinant3(flipRotation) = (1:R)228    rw [determinant3.value, e00, e01, e02, e10, e11, e12, e20, e21, e22]229    ring230  exact so3Matrices.mk with orthogonal, unit231232theorem flipRotation.pole (q : Set)233  requires sphere : q ∈ S²234  requires first : q(0) = (0:R)235  requires second : q(1) = (0:R)236  requires third : q(2) = -(1:R)237  shows flipRotation · q = basis(2)238proof239  have vector := S².function with sphere240  have matrix := flipRotation.matrix241  obtain ⟨e00, e01, e02, e10, e11, e12, e20, e21, e22⟩ :=242    flipRotation.entries243  have image := matrixVector.vector at flipRotation, q with *244  have pole := basis.vector at 2 with index.two_mem245  apply FunctionBetween.ext with image, pole246  intros i hi247  have entry := matrixVector.entry at flipRotation, q, i with *248  rw [entry, first, second, third]249  have alternatives := index.cases with hi250  rcases alternatives with at0 | at1 | at2251  . have other := basis.other at 0, 2252      with index.zero_mem, index.two_mem, index.zero_ne_two253    rw [at0, e00, e01, e02, other]254    ring255  . have other := basis.other at 1, 2256      with index.one_mem, index.two_mem, index.one_ne_two257    rw [at1, e10, e11, e12, other]258    ring259  . have same := basis.same at 2 with index.two_mem260    rw [at2, e20, e21, e22, same]261    ring262263-- Every point of the sphere is carried to the north pole by a rotation.264theorem so3.transitive_pole (q : Set)265  requires sphere : q ∈ S²266  shows ∃ σ ∈ so3Matrices, σ · q = basis(2)267proof268  have vector := S².function with sphere269  have q0 := vector.component_real at q, 0 with vector, index.zero_mem270  have q1 := vector.component_real at q, 1 with vector, index.one_mem271  have q2 := vector.component_real at q, 2 with vector, index.two_mem272  obtain ⟨inSpace, unit⟩ := S².membership.forward with sphere273  rw normSq.value at unit274  have alternatives : (q(2):R) = -(1:R) ∨ (q(2):R) ≠ -(1:R) by tauto275  cases alternatives with south | elsewhere276  . have squares : (q(0):R) * (q(0):R) + (q(1):R) * (q(1):R) = 0277      rw south at unit278      linear_combination unit279    have nonnegativeX := realMulValue.square_nonnegative at q(0)280    have nonnegativeY := realMulValue.square_nonnegative at q(1)281    have squareX := realAddValue.nonnegative_eq_zero at (q(0):R) * (q(0):R),282      (q(1):R) * (q(1):R) with nonnegativeX, nonnegativeY, squares283    have squareY : (q(1):R) * (q(1):R) = 0 by linarith284    have first := realMulValue.square_eq_zero_iff.forward with squareX285    have second := realMulValue.square_eq_zero_iff.forward with squareY286    have rotation := flipRotation.so3287    have pole := flipRotation.pole with sphere, first, second, south288    exact ⟨flipRotation, rotation, pole⟩289  . have nonzero : (1:R) + (q(2):R) ≠ 0290      intro zero291      apply elsewhere292      linarith293    have wReal := realInvValue.real at (1:R) + (q(2):R)294    have wz := realInvValue.mul_left at (1:R) + (q(2):R) with nonzero295    have rotation := poleRotation.so3 at q(0), q(1), q(2),296      realInvValue((1:R) + (q(2):R)) with unit, wz297    have pole := poleRotation.pole at q, realInvValue((1:R) + (q(2):R))298      with sphere, wz299    witness poleRotation(q(0), q(1), q(2), realInvValue((1:R) + (q(2):R)))300    exact ⟨rotation, pole⟩301