Grace/Cumulus/Geometry/Hausdorff/FixedPoints.g17

Open in Workbench Download source

Imports

Geometry.Vectors3 · Geometry.Absorption.Turn · Rotation.Freeness

Declarations

Source

1-- A rotation other than the identity fixes at most two points of the2-- sphere, a point and its antipode3-- 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.Hausdorff.FixedPoints9import Geometry.Vectors310import Geometry.Absorption.Turn11import Rotation.Freeness1213-- Three real squares summing to zero all vanish.14theorem sumSquares.eq_zero (a b c : Real)15  requires zero : a * a + b * b + c * c = 016  shows a = 0 ∧ b = 0 ∧ c = 017proof18  have squareA := realMulValue.square_nonnegative at a19  have squareB := realMulValue.square_nonnegative at b20  have squareC := realMulValue.square_nonnegative at c21  have zeroA : a * a = 0 by linarith22  have zeroB : b * b = 0 by linarith23  have zeroC : c * c = 0 by linarith24  have criterionA := realMulValue.square_eq_zero_iff at a25  have criterionB := realMulValue.square_eq_zero_iff at b26  have criterionC := realMulValue.square_eq_zero_iff at c27  exact ⟨criterionA.forward with zeroA, criterionB.forward with zeroB,28    criterionC.forward with zeroC⟩2930-- Two unit vectors that are neither equal nor opposite have a nonzero31-- cross product, by Lagrange's identity.32theorem cross.nonzero (u v : Set)33  requires memberU : u ∈ S²34  requires memberV : v ∈ S²35  requires distinct : v ≠ u36  requires opposite : v ≠ vectorNeg(u)37  shows normSq(cross(u, v)) ≠ (0:R)38proof39  obtain ⟨spaceU, unitU⟩ := S².membership.forward with memberU40  obtain ⟨spaceV, unitV⟩ := S².membership.forward with memberV41  have vectorU := ℝ³.function with spaceU42  have vectorV := ℝ³.function with spaceV43  have u0 := vector.component_real at u, 0 with vectorU, index.zero_mem44  have u1 := vector.component_real at u, 1 with vectorU, index.one_mem45  have u2 := vector.component_real at u, 2 with vectorU, index.two_mem46  have v0 := vector.component_real at v, 0 with vectorV, index.zero_mem47  have v1 := vector.component_real at v, 1 with vectorV, index.one_mem48  have v2 := vector.component_real at v, 2 with vectorV, index.two_mem49  have dotReal := dot3.real with vectorU, vectorV50  have lagrange := cross.normSq with vectorU, vectorV51  have dotValue := dot3.value at u, v52  rw [unitU, unitV] at lagrange53  rw normSq.value at unitU54  rw normSq.value at unitV55  intro zero56  rw zero at lagrange57  symm at lagrange58  have product : ((1:R) - dot3(u, v)) * ((1:R) + dot3(u, v)) =59      (0:R) * ((1:R) + dot3(u, v))60    linear_combination lagrange61  have split : (1:R) + dot3(u, v) = 0 ∨ (1:R) + dot3(u, v) ≠ 0 by tauto62  cases split with antipodal | generic63  . have sumZero : ((u(0):R) + (v(0):R)) * ((u(0):R) + (v(0):R)) +64        ((u(1):R) + (v(1):R)) * ((u(1):R) + (v(1):R)) +65        ((u(2):R) + (v(2):R)) * ((u(2):R) + (v(2):R)) = 066      linear_combination unitU + unitV - dotValue - dotValue + antipodal +67        antipodal68    obtain ⟨z0, z1, z2⟩ := sumSquares.eq_zero at (u(0):R) + (v(0):R),69      (u(1):R) + (v(1):R), (u(2):R) + (v(2):R) with sumZero70    apply opposite71    have negated := vectorNeg.vector with vectorU72    apply FunctionBetween.ext with vectorV, negated73    intros i hi74    have entry := vectorNeg.entry at u, i with vectorU, hi75    rw entry76    have alternatives := index.cases with hi77    rcases alternatives with at0 | at1 | at278    . rw at079      linarith80    . rw at181      linarith82    . rw at283      linarith84  . have cancel := realMulValue.right_cancel_of_nonzero at (1:R) - dot3(u, v),85      (0:R), (1:R) + dot3(u, v) with generic, product86    have sumZero : ((u(0):R) - (v(0):R)) * ((u(0):R) - (v(0):R)) +87        ((u(1):R) - (v(1):R)) * ((u(1):R) - (v(1):R)) +88        ((u(2):R) - (v(2):R)) * ((u(2):R) - (v(2):R)) = 089      linear_combination unitU + unitV + dotValue + dotValue + cancel + cancel90    obtain ⟨z0, z1, z2⟩ := sumSquares.eq_zero at (u(0):R) - (v(0):R),91      (u(1):R) - (v(1):R), (u(2):R) - (v(2):R) with sumZero92    apply distinct93    apply FunctionBetween.ext with vectorV, vectorU94    intros i hi95    have alternatives := index.cases with hi96    rcases alternatives with at0 | at1 | at297    . rw at098      linarith99    . rw at1100      linarith101    . rw at2102      linarith103104-- The three components of a vector are real.105theorem vector.components (x : Set)106  requires vector : x : 3 → ℝ107  shows x(0) ∈ ℝ ∧ x(1) ∈ ℝ ∧ x(2) ∈ ℝ108proof109  have x0 := vector.component_real at x, 0 with vector, index.zero_mem110  have x1 := vector.component_real at x, 1 with vector, index.one_mem111  have x2 := vector.component_real at x, 2 with vector, index.two_mem112  exact ⟨x0, x1, x2⟩113114-- The components of any vector r against the frame u, v, u × v: the115-- squared norm of u × v times r(k) is a combination of the dot products116-- of r with u, v, and u × v.117theorem cross.expand (u v r k : Set)118  requires vectorU : u : 3 → ℝ119  requires vectorV : v : 3 → ℝ120  requires vectorR : r : 3 → ℝ121  requires index : k ∈ 3122  shows normSq(cross(u, v)) * (r(k):R) =123    dot3(r, u) * (normSq(v) * (u(k):R) - dot3(u, v) * (v(k):R)) +124    dot3(r, v) * (normSq(u) * (v(k):R) - dot3(u, v) * (u(k):R)) +125    dot3(r, cross(u, v)) * (cross(u, v)(k):R)126proof127  have u0 := vector.component_real at u, 0 with vectorU, index.zero_mem128  have u1 := vector.component_real at u, 1 with vectorU, index.one_mem129  have u2 := vector.component_real at u, 2 with vectorU, index.two_mem130  have v0 := vector.component_real at v, 0 with vectorV, index.zero_mem131  have v1 := vector.component_real at v, 1 with vectorV, index.one_mem132  have v2 := vector.component_real at v, 2 with vectorV, index.two_mem133  have r0 := vector.component_real at r, 0 with vectorR, index.zero_mem134  have r1 := vector.component_real at r, 1 with vectorR, index.one_mem135  have r2 := vector.component_real at r, 2 with vectorR, index.two_mem136  have c0 := cross.zero with vectorU, vectorV137  have c1 := cross.one with vectorU, vectorV138  have c2 := cross.two with vectorU, vectorV139  have alternatives := index.cases with index140  rcases alternatives with at0 | at1 | at2141  . rw [at0, normSq.value, normSq.value, normSq.value, dot3.value, dot3.value,142      dot3.value, dot3.value, c0, c1, c2]143    ring144  . rw [at1, normSq.value, normSq.value, normSq.value, dot3.value, dot3.value,145      dot3.value, dot3.value, c0, c1, c2]146    ring147  . rw [at2, normSq.value, normSq.value, normSq.value, dot3.value, dot3.value,148      dot3.value, dot3.value, c0, c1, c2]149    ring150151-- A vector orthogonal to u, v, and u × v is zero when u × v is not.152theorem cross.orthogonal_zero (u v r : Set)153  requires vectorU : u : 3 → ℝ154  requires vectorV : v : 3 → ℝ155  requires vectorR : r : 3 → ℝ156  requires nonzero : normSq(cross(u, v)) ≠ (0:R)157  requires first : dot3(r, u) = (0:R)158  requires second : dot3(r, v) = (0:R)159  requires third : dot3(r, cross(u, v)) = (0:R)160  shows r = zeroVector161proof162  have zero := zeroVector.vector163  have wVector := cross.vector with vectorU, vectorV164  have normReal := normSq.real with wVector165  apply FunctionBetween.ext with vectorR, zero166  intros k hk167  have expand := cross.expand at u, v, r, k with vectorU, vectorV, vectorR, hk168  have component := vector.component_real at r, k with vectorR, hk169  have uk := vector.component_real at u, k with vectorU, hk170  have vk := vector.component_real at v, k with vectorV, hk171  have wk := vector.component_real at cross(u, v), k with wVector, hk172  obtain ⟨u0, u1, u2⟩ := vector.components with vectorU173  obtain ⟨v0, v1, v2⟩ := vector.components with vectorV174  obtain ⟨w0, w1, w2⟩ := vector.components with wVector175  rw [first, second, third] at expand176  have same : (r(k):R) * normSq(cross(u, v)) = (0:R) * normSq(cross(u, v))177    linear_combination expand178  have vanishes := realMulValue.right_cancel_of_nonzero at (r(k):R), (0:R),179    normSq(cross(u, v)) with nonzero, same180  rw zeroVector.entry181  exact vanishes182183-- The dot product with a basis vector picks a component.184theorem basis.dot (x i : Set)185  requires vector : x : 3 → ℝ186  requires index : i ∈ 3187  shows (basis(i)(0):R) * (x(0):R) + (basis(i)(1):R) * (x(1):R) +188    (basis(i)(2):R) * (x(2):R) = (x(i):R)189proof190  have x0 := vector.component_real at x, 0 with vector, index.zero_mem191  have x1 := vector.component_real at x, 1 with vector, index.one_mem192  have x2 := vector.component_real at x, 2 with vector, index.two_mem193  have alternatives := index.cases with index194  rcases alternatives with at0 | at1 | at2195  . have same := basis.same at 0 with index.zero_mem196    have other1 := basis.other at 1, 0197      with index.one_mem, index.zero_mem, index.one_ne_zero198    have other2 := basis.other at 2, 0199      with index.two_mem, index.zero_mem, index.two_ne_zero200    rw [at0, same, other1, other2]201    ring202  . have same := basis.same at 1 with index.one_mem203    have other0 := basis.other at 0, 1204      with index.zero_mem, index.one_mem, index.zero_ne_one205    have other2 := basis.other at 2, 1206      with index.two_mem, index.one_mem, index.two_ne_one207    rw [at1, same, other0, other2]208    ring209  . have same := basis.same at 2 with index.two_mem210    have other0 := basis.other at 0, 2211      with index.zero_mem, index.two_mem, index.zero_ne_two212    have other1 := basis.other at 1, 2213      with index.one_mem, index.two_mem, index.one_ne_two214    rw [at2, same, other0, other1]215    ring216217-- Row i of M − 1, as a vector.218defgraph rowShift (M i : Set) (k ∈ 3) : ℝ := (M[i, k]:R) - (basis(i)(k):R)219requires matrix : M : realRing ^ 3 × 3220requires row : i ∈ 3221proof222  have entry := Matrix.real_entry at M, i, k with matrix, row, member223  have basisVector := basis.vector with row224  have component := vector.component_real at basis(i), k225    with basisVector, member226  typecheck227228instance rowShift.vector (M i : Set)229  requires matrix : M : realRing ^ 3 × 3230  requires row : i ∈ 3231  shows rowShift(M, i) : 3 → ℝ232proof233  exact rowShift.function with matrix, row234235theorem rowShift.entry (M i k : Set)236  requires matrix : M : realRing ^ 3 × 3237  requires row : i ∈ 3238  requires column : k ∈ 3239  shows rowShift(M, i)(k) = (M[i, k]:R) - (basis(i)(k):R)240proof241  exact rowShift.value with matrix, row, column242243-- A row of M − 1 is orthogonal to every vector fixed by M.244theorem rowShift.dot (M i x : Set)245  requires matrix : M : realRing ^ 3 × 3246  requires row : i ∈ 3247  requires vector : x : 3 → ℝ248  requires fixed : M · x = x249  shows dot3(rowShift(M, i), x) = (0:R)250proof251  have entry := matrixVector.entry at M, x, i with matrix, vector, row252  rw fixed at entry253  have basisDot := basis.dot with vector, row254  have basisVector := basis.vector with row255  have b0 := vector.component_real at basis(i), 0256    with basisVector, index.zero_mem257  have b1 := vector.component_real at basis(i), 1258    with basisVector, index.one_mem259  have b2 := vector.component_real at basis(i), 2260    with basisVector, index.two_mem261  obtain ⟨m0, m1, m2⟩ := Matrix.row_real at M, i with row262  have x0 := vector.component_real at x, 0 with vector, index.zero_mem263  have x1 := vector.component_real at x, 1 with vector, index.one_mem264  have x2 := vector.component_real at x, 2 with vector, index.two_mem265  have xi := vector.component_real at x, i with vector, row266  have r0 := rowShift.entry at M, i, 0 with matrix, row, index.zero_mem267  have r1 := rowShift.entry at M, i, 1 with matrix, row, index.one_mem268  have r2 := rowShift.entry at M, i, 2 with matrix, row, index.two_mem269  rw [dot3.value, r0, r1, r2]270  symm at entry271  linear_combination entry - basisDot272273-- The drift of row i: the component of row i of M − 1 along u × v.274def drift (M u v i : Set) : Set := dot3(rowShift(M, i), cross(u, v))275276theorem drift.value (M u v i : Set)277  shows drift(M, u, v, i) = dot3(rowShift(M, i), cross(u, v))278proof279  simp [drift]280281instance drift.real (M u v i : Set)282  requires matrix : M : realRing ^ 3 × 3283  requires vectorU : u : 3 → ℝ284  requires vectorV : v : 3 → ℝ285  requires row : i ∈ 3286  shows drift(M, u, v, i) ∈ ℝ287proof288  have shift := rowShift.vector with matrix, row289  have wVector := cross.vector with vectorU, vectorV290  rw drift.value291  exact dot3.real with shift, wVector292293-- When M fixes u and v, the entries of M are those of the identity plus294-- the drift of the row times u × v, up to the factor |u × v|².295theorem fixed.entry (M u v i k : Set)296  requires matrix : M : realRing ^ 3 × 3297  requires vectorU : u : 3 → ℝ298  requires vectorV : v : 3 → ℝ299  requires fixedU : M · u = u300  requires fixedV : M · v = v301  requires row : i ∈ 3302  requires column : k ∈ 3303  shows normSq(cross(u, v)) * (M[i, k]:R) =304    normSq(cross(u, v)) * (basis(i)(k):R) +305    drift(M, u, v, i) * (cross(u, v)(k):R)306proof307  have shift := rowShift.vector with matrix, row308  have expand := cross.expand at u, v, rowShift(M, i), k309    with vectorU, vectorV, shift, column310  have first := rowShift.dot with matrix, row, vectorU, fixedU311  have second := rowShift.dot with matrix, row, vectorV, fixedV312  have entry := rowShift.entry at M, i, k with matrix, row, column313  have wVector := cross.vector with vectorU, vectorV314  have uk := vector.component_real at u, k with vectorU, column315  have vk := vector.component_real at v, k with vectorV, column316  have wk := vector.component_real at cross(u, v), k with wVector, column317  obtain ⟨u0, u1, u2⟩ := vector.components with vectorU318  obtain ⟨v0, v1, v2⟩ := vector.components with vectorV319  obtain ⟨w0, w1, w2⟩ := vector.components with wVector320  obtain ⟨s0, s1, s2⟩ := vector.components with shift321  have mik := Matrix.real_entry at M, i, k with matrix, row, column322  have basisVector := basis.vector with row323  have bik := vector.component_real at basis(i), k324    with basisVector, column325  rw [first, second, entry] at expand326  rw drift.value327  linear_combination expand328329-- A rotation fixing two unit vectors that are neither equal nor opposite330-- is the identity.331theorem so3.fixed_pair (M u v : Set)332  requires member : M ∈ so3Matrices333  requires memberU : u ∈ S²334  requires memberV : v ∈ S²335  requires fixedU : M · u = u336  requires fixedV : M · v = v337  requires distinct : v ≠ u338  requires opposite : v ≠ vectorNeg(u)339  shows M = Ring.one(matrixRing(realRing, 3))340proof341  have comm := realRing.comm_ring342  have matrix := so3Matrices.matrix with member343  have orthogonal := so3Matrices.orthogonal with member344  have unit := so3Matrices.determinant with member345  have one := Matrix.one_matrix346  have nonzero := cross.nonzero with memberU, memberV, distinct, opposite347  have vectorU := S².function with memberU348  have vectorV := S².function with memberV349  have wVector := cross.vector with vectorU, vectorV350  have normReal := normSq.real with wVector351  have normValue := normSq.value at cross(u, v)352  obtain ⟨w0, w1, w2⟩ := vector.components with wVector353  obtain ⟨u0, u1, u2⟩ := vector.components with vectorU354  obtain ⟨v0, v1, v2⟩ := vector.components with vectorV355  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ :=356    Matrix.entries_real with matrix357  have shift0 := rowShift.vector at M, 0 with matrix, index.zero_mem358  have shift1 := rowShift.vector at M, 1 with matrix, index.one_mem359  have shift2 := rowShift.vector at M, 2 with matrix, index.two_mem360  obtain ⟨s00, s01, s02⟩ := vector.components with shift0361  obtain ⟨s10, s11, s12⟩ := vector.components with shift1362  obtain ⟨s20, s21, s22⟩ := vector.components with shift2363  have d0 := drift.real at M, u, v, 0364    with matrix, vectorU, vectorV, index.zero_mem365  have d1 := drift.real at M, u, v, 1366    with matrix, vectorU, vectorV, index.one_mem367  have d2 := drift.real at M, u, v, 2368    with matrix, vectorU, vectorV, index.two_mem369  have b00 := basis.same at 0 with index.zero_mem370  have b11 := basis.same at 1 with index.one_mem371  have b22 := basis.same at 2 with index.two_mem372  have b01 := basis.other at 1, 0373    with index.one_mem, index.zero_mem, index.one_ne_zero374  have b02 := basis.other at 2, 0375    with index.two_mem, index.zero_mem, index.two_ne_zero376  have b10 := basis.other at 0, 1377    with index.zero_mem, index.one_mem, index.zero_ne_one378  have b12 := basis.other at 2, 1379    with index.two_mem, index.one_mem, index.two_ne_one380  have b20 := basis.other at 0, 2381    with index.zero_mem, index.two_mem, index.zero_ne_two382  have b21 := basis.other at 1, 2383    with index.one_mem, index.two_mem, index.one_ne_two384  have entries : ∀ i ∈ 3, ∀ k ∈ 3, normSq(cross(u, v)) * (M[i, k]:R) =385      normSq(cross(u, v)) * (basis(i)(k):R) +386      drift(M, u, v, i) * (cross(u, v)(k):R)387    intros i hi k hk388    exact fixed.entry with matrix, vectorU, vectorV, fixedU, fixedV, hi, hk389  have e00 := entries with 0, index.zero_mem, 0, index.zero_mem390  have e01 := entries with 0, index.zero_mem, 1, index.one_mem391  have e02 := entries with 0, index.zero_mem, 2, index.two_mem392  have e10 := entries with 1, index.one_mem, 0, index.zero_mem393  have e11 := entries with 1, index.one_mem, 1, index.one_mem394  have e12 := entries with 1, index.one_mem, 2, index.two_mem395  have e20 := entries with 2, index.two_mem, 0, index.zero_mem396  have e21 := entries with 2, index.two_mem, 1, index.one_mem397  have e22 := entries with 2, index.two_mem, 2, index.two_mem398  rw b00 at e00399  rw b01 at e01400  rw b02 at e02401  rw b10 at e10402  rw b11 at e11403  rw b12 at e12404  rw b20 at e20405  rw b21 at e21406  rw b22 at e22407  -- The determinant: 1 = det M, and |w|⁶ det M expands through the entries.408  have detValue := determinant3.value at M409  rw unit at detValue410  have cubic : normSq(cross(u, v)) * normSq(cross(u, v)) *411      normSq(cross(u, v)) * (1:R) =412      (normSq(cross(u, v)) * (M[0, 0]:R)) *413        ((normSq(cross(u, v)) * (M[1, 1]:R)) *414          (normSq(cross(u, v)) * (M[2, 2]:R)) -415         (normSq(cross(u, v)) * (M[1, 2]:R)) *416          (normSq(cross(u, v)) * (M[2, 1]:R))) -417      (normSq(cross(u, v)) * (M[0, 1]:R)) *418        ((normSq(cross(u, v)) * (M[1, 0]:R)) *419          (normSq(cross(u, v)) * (M[2, 2]:R)) -420         (normSq(cross(u, v)) * (M[1, 2]:R)) *421          (normSq(cross(u, v)) * (M[2, 0]:R))) +422      (normSq(cross(u, v)) * (M[0, 2]:R)) *423        ((normSq(cross(u, v)) * (M[1, 0]:R)) *424          (normSq(cross(u, v)) * (M[2, 1]:R)) -425         (normSq(cross(u, v)) * (M[1, 1]:R)) *426          (normSq(cross(u, v)) * (M[2, 0]:R)))427    rw detValue428    ring429  rw [e00, e01, e02, e10, e11, e12, e20, e21, e22] at cubic430  have driftScaled : (normSq(cross(u, v)) *431      (drift(M, u, v, 0) * (cross(u, v)(0):R) +432        drift(M, u, v, 1) * (cross(u, v)(1):R) +433        drift(M, u, v, 2) * (cross(u, v)(2):R))) *434      normSq(cross(u, v)) = (0:R) * normSq(cross(u, v))435    symm at cubic436    linear_combination cubic437  have driftOnce := realMulValue.right_cancel_of_nonzero at438    normSq(cross(u, v)) * (drift(M, u, v, 0) * (cross(u, v)(0):R) +439      drift(M, u, v, 1) * (cross(u, v)(1):R) +440      drift(M, u, v, 2) * (cross(u, v)(2):R)),441    (0:R), normSq(cross(u, v)) with nonzero, driftScaled442  have driftTwice : (drift(M, u, v, 0) * (cross(u, v)(0):R) +443      drift(M, u, v, 1) * (cross(u, v)(1):R) +444      drift(M, u, v, 2) * (cross(u, v)(2):R)) *445      normSq(cross(u, v)) = (0:R) * normSq(cross(u, v))446    linear_combination driftOnce447  have driftDot := realMulValue.right_cancel_of_nonzero at448    drift(M, u, v, 0) * (cross(u, v)(0):R) +449      drift(M, u, v, 1) * (cross(u, v)(1):R) +450      drift(M, u, v, 2) * (cross(u, v)(2):R), (0:R), normSq(cross(u, v))451    with nonzero, driftTwice452  -- The image of w: M · w = w + drift, and it has the length of w.453  have image := matrixVector.vector with matrix, wVector454  have moved : ∀ i ∈ 3,455      ((M · cross(u, v))(i):R) = (cross(u, v)(i):R) + drift(M, u, v, i)456    intros i hi457    have entry := matrixVector.entry at M, cross(u, v), i458      with matrix, wVector, hi459    have component := vector.component_real at M · cross(u, v), i460      with image, hi461    have wi := vector.component_real at cross(u, v), i with wVector, hi462    have driftI := drift.real at M, u, v, i with matrix, vectorU, vectorV, hi463    have shiftI := rowShift.vector at M, i with matrix, hi464    obtain ⟨si0, si1, si2⟩ := vector.components with shiftI465    have basisDot := basis.dot with wVector, hi466    have basisVector := basis.vector with hi467    have b0 := vector.component_real at basis(i), 0468      with basisVector, index.zero_mem469    have b1 := vector.component_real at basis(i), 1470      with basisVector, index.one_mem471    have b2 := vector.component_real at basis(i), 2472      with basisVector, index.two_mem473    obtain ⟨mi0, mi1, mi2⟩ := Matrix.row_real at M, i with hi474    have f0 := entries with i, hi, 0, index.zero_mem475    have f1 := entries with i, hi, 1, index.one_mem476    have f2 := entries with i, hi, 2, index.two_mem477    have same : ((M · cross(u, v))(i):R) * normSq(cross(u, v)) =478        ((cross(u, v)(i):R) + drift(M, u, v, i)) * normSq(cross(u, v))479      linear_combination normSq(cross(u, v)) * entry + (cross(u, v)(0):R) * f0 +480        (cross(u, v)(1):R) * f1 + (cross(u, v)(2):R) * f2 +481        normSq(cross(u, v)) * basisDot - drift(M, u, v, i) * normValue482    exact realMulValue.right_cancel_of_nonzero at ((M · cross(u, v))(i):R),483      (cross(u, v)(i):R) + drift(M, u, v, i), normSq(cross(u, v))484      with nonzero, same485  have moved0 := moved with 0, index.zero_mem486  have moved1 := moved with 1, index.one_mem487  have moved2 := moved with 2, index.two_mem488  have norm := Orthogonal.normSq with orthogonal, wVector489  rw [normSq.value, normSq.value, moved0, moved1, moved2] at norm490  have squares : drift(M, u, v, 0) * drift(M, u, v, 0) +491      drift(M, u, v, 1) * drift(M, u, v, 1) +492      drift(M, u, v, 2) * drift(M, u, v, 2) = 0493    linear_combination norm - driftDot - driftDot494  obtain ⟨z0, z1, z2⟩ := sumSquares.eq_zero at drift(M, u, v, 0),495    drift(M, u, v, 1), drift(M, u, v, 2) with squares496  have driftZero : ∀ i ∈ 3, drift(M, u, v, i) = 0497    intros i hi498    have alternatives := index.cases with hi499    rcases alternatives with at0 | at1 | at2500    . rw at0501      exact z0502    . rw at1503      exact z1504    . rw at2505      exact z2506  -- Every entry of M is the matching entry of the identity.507  apply Matrix.ext with matrix, one508  intros i hi j hj509  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) :=510    Ring.zero_mem with *511  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) :=512    Ring.one_mem with *513  have shape := entries with i, hi, j, hj514  have vanish := driftZero with i, hi515  rw vanish at shape516  have shiftI := rowShift.vector at M, i with matrix, hi517  obtain ⟨si0, si1, si2⟩ := vector.components with shiftI518  have basisVector := basis.vector with hi519  have bij := vector.component_real at basis(i), j520    with basisVector, hj521  have mij := Matrix.real_entry at M, i, j with matrix, hi, hj522  have wj := vector.component_real at cross(u, v), j with wVector, hj523  have same : (M[i, j]:R) * normSq(cross(u, v)) =524      (basis(i)(j):R) * normSq(cross(u, v))525    linear_combination shape526  have entry := realMulValue.right_cancel_of_nonzero at (M[i, j]:R),527    (basis(i)(j):R), normSq(cross(u, v)) with nonzero, same528  have basisValue := basis.value at i, j with hi, hj529  have symmetric := singleValue.symmetric at i, j530  have oneEntry := matrixRing.one_entry at realRing, 3, i, j with comm, hi, hj531  rw [entry, basisValue, oneEntry, symmetric]532  rfl533534-- A rotation that is not the identity fixes at most two points of the535-- sphere, a point and its opposite.536theorem so3.fixed_points (M : Set)537  requires member : M ∈ so3Matrices538  requires nontrivial : M ≠ Ring.one(matrixRing(realRing, 3))539  shows ∃ p ∈ S², ∀ v ∈ S², M · v = v → v = p ∨ v = vectorNeg(p)540proof541  have split : (∃ u ∈ S², M · u = u) ∨ ¬(∃ u ∈ S², M · u = u)542    tauto543  cases split with some | none544  . obtain ⟨u, hu, fixedU⟩ := some545    refine ⟨u, hu, ?_⟩546    intros v hv fixedV547    by_contra548    have distinct : v ≠ u549      intro equal550      apply this551      left552      exact equal553    have opposite : v ≠ vectorNeg(u)554      intro equal555      apply this556      right557      exact equal558    have identity := so3.fixed_pair with member, hu, hv, fixedU, fixedV,559      distinct, opposite560    exact nontrivial with identity561  . have poleVector := basis.vector at 2 with index.two_mem562    have poleSpace := ℝ³.of_function with poleVector563    have same := basis.same at 2 with index.two_mem564    have other0 := basis.other at 0, 2565      with index.zero_mem, index.two_mem, index.zero_ne_two566    have other1 := basis.other at 1, 2567      with index.one_mem, index.two_mem, index.one_ne_two568    have poleUnit : normSq(basis(2)) = (1:R)569      rw [normSq.value, same, other0, other1]570      ring571    have poleIn := S².membership.backward at basis(2)572      with ⟨poleSpace, poleUnit⟩573    refine ⟨basis(2), poleIn, ?_⟩574    intros v hv fixedV575    exfalso576    apply none577    exact ⟨v, hv, fixedV⟩578