Grace/Cumulus/Rotation/Freeness.g17

Open in Workbench Download source

Imports

Generators · Algebra.Group.Words · Real.Integer

Declarations

Source

1-- The rotation of a word in the generators a, a⁻¹, b, b⁻¹ and the freeness2-- theorem: a nonempty reduced word is not the identity rotation, by3-- Swierczkowski's argument on integer vectors modulo 54-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Rotation.Freeness10import Generators11import Algebra.Group.Words12import Real.Integer1314-- The matrix of a letter: 0, 1, 2, 3 read rotA, rotA⁻¹, rotB, rotB⁻¹.15def letterMatrix (ℓ : Nat) → Set16  | zero => rotA17  | succ(k) => pick3(transpose(rotA), rotB, transpose(rotB), k)1819theorem letterMatrix.zero20  shows letterMatrix(0) = rotA21proof22  simp [letterMatrix]2324theorem letterMatrix.one25  shows letterMatrix(1) = transpose(rotA)26proof27  simp [letterMatrix, pick3]2829theorem letterMatrix.two30  shows letterMatrix(2) = rotB31proof32  simp [letterMatrix, pick3, pick2]3334theorem letterMatrix.three35  shows letterMatrix(3) = transpose(rotB)36proof37  simp [letterMatrix, pick3, pick2]3839theorem letterMatrix.so3 (ℓ : Set)40  requires letter : ℓ ∈ 441  shows letterMatrix(ℓ) ∈ so3Matrices42proof43  have alternatives := letter.cases with letter44  rcases alternatives with at0 | at1 | at2 | at345  . rw [at0, letterMatrix.zero]46    exact rotA.so347  . rw [at1, letterMatrix.one]48    exact rotA.transpose_so349  . rw [at2, letterMatrix.two]50    exact rotB.so351  . rw [at3, letterMatrix.three]52    exact rotB.transpose_so35354instance letterMatrix.matrix (ℓ : Set)55  requires letter : ℓ ∈ 456  shows letterMatrix(ℓ) : realRing ^ 3 × 357proof58  exact so3Matrices.matrix with (letterMatrix.so3 with letter)5960-- The rotation of a word: the product of the matrices of its letters.61def wordRotation (w : List(4)) → Set62  | [] => Ring.one(matrixRing(realRing, 3))63  | ℓ :: rest => call2(Ring.mul(matrixRing(realRing, 3)), letterMatrix(ℓ), wordRotation(rest))6465theorem wordRotation.nil66  shows wordRotation([]) = Ring.one(matrixRing(realRing, 3))67proof68  simp [wordRotation]6970theorem wordRotation.cons (ℓ : Set) (rest : List(4))71  requires letter : ℓ ∈ 472  shows wordRotation(ℓ :: rest) =73    Ring.mul(matrixRing(realRing, 3))(letterMatrix(ℓ), wordRotation(rest))74proof75  simp [wordRotation]7677theorem wordRotation.so3 (w : List(4))78  shows wordRotation(w) ∈ so3Matrices79proof80  induction w81  | List.nil =>82    rw wordRotation.nil83    exact so3Matrices.one_mem84  | List.cons(ℓ, rest) using ih =>85    have letter : ℓ ∈ 4 by assumption86    have head := letterMatrix.so3 with letter87    have headMatrix := so3Matrices.matrix with head88    have restMatrix := so3Matrices.matrix with ih89    rw wordRotation.cons90    exact so3Matrices.mul_mem with head, ih9192instance wordRotation.matrix (w : List(4))93  shows wordRotation(w) : realRing ^ 3 × 394proof95  have member := wordRotation.so3 at w with *96  exact so3Matrices.matrix with member9798-- The scale 5^k of a word of length k, as a recursion on the word.99def fivePow (w : List(4)) → Set100  | [] => (1:R)101  | ℓ :: rest => (5:R) * (fivePow(rest):R)102103theorem fivePow.nil104  shows fivePow([]) = (1:R)105proof106  simp [fivePow]107108theorem fivePow.cons (ℓ : Set) (rest : List(4))109  requires letter : ℓ ∈ 4110  shows fivePow(ℓ :: rest) = (5:R) * (fivePow(rest):R)111proof112  simp [fivePow]113114instance fivePow.real (w : List(4))115  shows fivePow(w) ∈ ℝ116proof117  induction w118  | List.nil =>119    rw fivePow.nil120    typecheck121  | List.cons(ℓ, rest) using ih =>122    have letter : ℓ ∈ 4 by assumption123    rw fivePow.cons124    typecheck125126-- The scaled coordinates of the path of a word from a start vector v:127-- 5^k times the i-th coordinate of wordRotation(w) · v.128def coordinate (w v i : Set) : Set :=129  (fivePow(w):R) * ((wordRotation(w) · v)(i):R)130131theorem coordinate.value (w v i : Set)132  shows coordinate(w, v, i) = (fivePow(w):R) * ((wordRotation(w) · v)(i):R)133proof134  simp [coordinate]135136-- Five times the action of each generator, in integer form.137theorem rotA.five_action (u : Set)138  requires vector : u : 3 → ℝ139  shows (5:R) * ((rotA · u)(0):R) = 5 * (u(0):R) ∧140    (5:R) * ((rotA · u)(1):R) = 3 * (u(1):R) - 4 * (u(2):R) ∧141    (5:R) * ((rotA · u)(2):R) = 4 * (u(1):R) + 3 * (u(2):R)142proof143  obtain ⟨a00, a01, a02, a10, a11, a12, a20, a21, a22⟩ := rotA.entries144  have five := fifth.five145  have u0 := vector.component_real at u, 0 with *146  have u1 := vector.component_real at u, 1 with *147  have u2 := vector.component_real at u, 2 with *148  have e0 := matrixVector.entry at rotA, u, 0 with *149  have e1 := matrixVector.entry at rotA, u, 1 with *150  have e2 := matrixVector.entry at rotA, u, 2 with *151  rw [e0, e1, e2, a00, a01, a02, a10, a11, a12, a20, a21, a22]152  have scale1 : fifth * 5 * (3 * (u(1):R) - 4 * (u(2):R)) = 3 * (u(1):R) - 4 * (u(2):R)153    rw five154    ring155  have scale2 : fifth * 5 * (4 * (u(1):R) + 3 * (u(2):R)) = 4 * (u(1):R) + 3 * (u(2):R)156    rw five157    ring158  constructor159  . ring160  . constructor161    . calc162        (5:R) * ((0:R) * (u(0):R) + 3 * fifth * (u(1):R) + -(4 * fifth) * (u(2):R)) =163            fifth * 5 * (3 * (u(1):R) - 4 * (u(2):R)) := by ring164        _ = 3 * (u(1):R) - 4 * (u(2):R) := scale1165    . calc166        (5:R) * ((0:R) * (u(0):R) + 4 * fifth * (u(1):R) + 3 * fifth * (u(2):R)) =167            fifth * 5 * (4 * (u(1):R) + 3 * (u(2):R)) := by ring168        _ = 4 * (u(1):R) + 3 * (u(2):R) := scale2169170theorem rotA.transpose_five_action (u : Set)171  requires vector : u : 3 → ℝ172  shows (5:R) * ((transpose(rotA) · u)(0):R) = 5 * (u(0):R) ∧173    (5:R) * ((transpose(rotA) · u)(1):R) = 3 * (u(1):R) + 4 * (u(2):R) ∧174    (5:R) * ((transpose(rotA) · u)(2):R) = 3 * (u(2):R) - 4 * (u(1):R)175proof176  obtain ⟨a00, a01, a02, a10, a11, a12, a20, a21, a22⟩ := rotA.entries177  have five := fifth.five178  have transposed := transpose.matrix at rotA with *179  have u0 := vector.component_real at u, 0 with *180  have u1 := vector.component_real at u, 1 with *181  have u2 := vector.component_real at u, 2 with *182  have e0 := matrixVector.entry at transpose(rotA), u, 0 with *183  have e1 := matrixVector.entry at transpose(rotA), u, 1 with *184  have e2 := matrixVector.entry at transpose(rotA), u, 2 with *185  have t00 := transpose.entry at rotA, 0, 0 with *186  have t01 := transpose.entry at rotA, 0, 1 with *187  have t02 := transpose.entry at rotA, 0, 2 with *188  have t10 := transpose.entry at rotA, 1, 0 with *189  have t11 := transpose.entry at rotA, 1, 1 with *190  have t12 := transpose.entry at rotA, 1, 2 with *191  have t20 := transpose.entry at rotA, 2, 0 with *192  have t21 := transpose.entry at rotA, 2, 1 with *193  have t22 := transpose.entry at rotA, 2, 2 with *194  rw [e0, e1, e2, t00, t01, t02, t10, t11, t12, t20, t21, t22,195    a00, a01, a02, a10, a11, a12, a20, a21, a22]196  have scale1 : fifth * 5 * (3 * (u(1):R) + 4 * (u(2):R)) = 3 * (u(1):R) + 4 * (u(2):R)197    rw five198    ring199  have scale2 : fifth * 5 * (3 * (u(2):R) - 4 * (u(1):R)) = 3 * (u(2):R) - 4 * (u(1):R)200    rw five201    ring202  constructor203  . ring204  . constructor205    . calc206        (5:R) * ((0:R) * (u(0):R) + 3 * fifth * (u(1):R) + 4 * fifth * (u(2):R)) =207            fifth * 5 * (3 * (u(1):R) + 4 * (u(2):R)) := by ring208        _ = 3 * (u(1):R) + 4 * (u(2):R) := scale1209    . calc210        (5:R) * ((0:R) * (u(0):R) + -(4 * fifth) * (u(1):R) + 3 * fifth * (u(2):R)) =211            fifth * 5 * (3 * (u(2):R) - 4 * (u(1):R)) := by ring212        _ = 3 * (u(2):R) - 4 * (u(1):R) := scale2213214theorem rotB.five_action (u : Set)215  requires vector : u : 3 → ℝ216  shows (5:R) * ((rotB · u)(0):R) = 3 * (u(0):R) - 4 * (u(1):R) ∧217    (5:R) * ((rotB · u)(1):R) = 4 * (u(0):R) + 3 * (u(1):R) ∧218    (5:R) * ((rotB · u)(2):R) = 5 * (u(2):R)219proof220  obtain ⟨b00, b01, b02, b10, b11, b12, b20, b21, b22⟩ := rotB.entries221  have five := fifth.five222  have u0 := vector.component_real at u, 0 with *223  have u1 := vector.component_real at u, 1 with *224  have u2 := vector.component_real at u, 2 with *225  have e0 := matrixVector.entry at rotB, u, 0 with *226  have e1 := matrixVector.entry at rotB, u, 1 with *227  have e2 := matrixVector.entry at rotB, u, 2 with *228  rw [e0, e1, e2, b00, b01, b02, b10, b11, b12, b20, b21, b22]229  have scale0 : fifth * 5 * (3 * (u(0):R) - 4 * (u(1):R)) = 3 * (u(0):R) - 4 * (u(1):R)230    rw five231    ring232  have scale1 : fifth * 5 * (4 * (u(0):R) + 3 * (u(1):R)) = 4 * (u(0):R) + 3 * (u(1):R)233    rw five234    ring235  constructor236  . calc237      (5:R) * (3 * fifth * (u(0):R) + -(4 * fifth) * (u(1):R) + (0:R) * (u(2):R)) =238          fifth * 5 * (3 * (u(0):R) - 4 * (u(1):R)) := by ring239      _ = 3 * (u(0):R) - 4 * (u(1):R) := scale0240  . constructor241    . calc242        (5:R) * (4 * fifth * (u(0):R) + 3 * fifth * (u(1):R) + (0:R) * (u(2):R)) =243            fifth * 5 * (4 * (u(0):R) + 3 * (u(1):R)) := by ring244        _ = 4 * (u(0):R) + 3 * (u(1):R) := scale1245    . ring246247theorem rotB.transpose_five_action (u : Set)248  requires vector : u : 3 → ℝ249  shows (5:R) * ((transpose(rotB) · u)(0):R) = 3 * (u(0):R) + 4 * (u(1):R) ∧250    (5:R) * ((transpose(rotB) · u)(1):R) = 3 * (u(1):R) - 4 * (u(0):R) ∧251    (5:R) * ((transpose(rotB) · u)(2):R) = 5 * (u(2):R)252proof253  obtain ⟨b00, b01, b02, b10, b11, b12, b20, b21, b22⟩ := rotB.entries254  have five := fifth.five255  have transposed := transpose.matrix at rotB with *256  have u0 := vector.component_real at u, 0 with *257  have u1 := vector.component_real at u, 1 with *258  have u2 := vector.component_real at u, 2 with *259  have e0 := matrixVector.entry at transpose(rotB), u, 0 with *260  have e1 := matrixVector.entry at transpose(rotB), u, 1 with *261  have e2 := matrixVector.entry at transpose(rotB), u, 2 with *262  have t00 := transpose.entry at rotB, 0, 0 with *263  have t01 := transpose.entry at rotB, 0, 1 with *264  have t02 := transpose.entry at rotB, 0, 2 with *265  have t10 := transpose.entry at rotB, 1, 0 with *266  have t11 := transpose.entry at rotB, 1, 1 with *267  have t12 := transpose.entry at rotB, 1, 2 with *268  have t20 := transpose.entry at rotB, 2, 0 with *269  have t21 := transpose.entry at rotB, 2, 1 with *270  have t22 := transpose.entry at rotB, 2, 2 with *271  rw [e0, e1, e2, t00, t01, t02, t10, t11, t12, t20, t21, t22,272    b00, b01, b02, b10, b11, b12, b20, b21, b22]273  have scale0 : fifth * 5 * (3 * (u(0):R) + 4 * (u(1):R)) = 3 * (u(0):R) + 4 * (u(1):R)274    rw five275    ring276  have scale1 : fifth * 5 * (3 * (u(1):R) - 4 * (u(0):R)) = 3 * (u(1):R) - 4 * (u(0):R)277    rw five278    ring279  constructor280  . calc281      (5:R) * (3 * fifth * (u(0):R) + 4 * fifth * (u(1):R) + (0:R) * (u(2):R)) =282          fifth * 5 * (3 * (u(0):R) + 4 * (u(1):R)) := by ring283      _ = 3 * (u(0):R) + 4 * (u(1):R) := scale0284  . constructor285    . calc286        (5:R) * (-(4 * fifth) * (u(0):R) + 3 * fifth * (u(1):R) + (0:R) * (u(2):R)) =287            fifth * 5 * (3 * (u(1):R) - 4 * (u(0):R)) := by ring288        _ = 3 * (u(1):R) - 4 * (u(0):R) := scale1289    . ring290291-- Integer-valued reals, as differences of naturals, and the multiples of292-- five among them.293predicate IntReal (x : Set) :=294  ∃ m ∈ ℕ, ∃ n ∈ ℕ, x = (realNat(m):R) - (realNat(n):R)295predicate Div5 (x : Set) :=296  ∃ m ∈ ℕ, ∃ n ∈ ℕ, x = 5 * (realNat(m):R) - 5 * (realNat(n):R)297298theorem IntReal.real (x : Set)299  requires integral : IntReal(x)300  shows x ∈ ℝ301proof302  obtain ⟨m, hm, n, hn, equal⟩ := integral303  have natM := nat.omega.backward with hm304  have natN := nat.omega.backward with hn305  rw equal306  typecheck307308-- The integer-valued reals are exactly the image of ℤ under realInt.309theorem IntReal.iff_realInt (x : Set)310  shows IntReal(x) ↔ ∃ z ∈ ℤ, x = realInt(z)311proof312  have range := realInt.range at x313  unfold IntReal314  constructor315  . intro difference316    exact range.backward with difference317  . intro image318    exact range.forward with image319320theorem IntReal.nat (k : Nat)321  shows IntReal(realNat(k))322proof323  have kIn : k ∈ ℕ := nat.omega.forward with assumption324  have zeroIn : 0 ∈ ℕ := nat.omega.forward at 0 with *325  unfold IntReal326  refine ⟨k, kIn, 0, zeroIn, ?_⟩327  rw realNat.zero328  ring329330theorem IntReal.numeral (k : Nat)331  shows IntReal(realNumeral(k))332proof333  unfold realNumeral334  exact IntReal.nat at k335336theorem IntReal.zero337  shows IntReal((0:R))338proof339  have natural := IntReal.nat at 0340  rw realNat.zero at natural341  exact natural342343theorem IntReal.one344  shows IntReal((1:R))345proof346  have natural := IntReal.nat at 1347  rw realNat.one at natural348  exact natural349350theorem IntReal.add (x y : Set)351  requires integralX : IntReal(x)352  requires integralY : IntReal(y)353  shows IntReal((x:R) + (y:R))354proof355  obtain ⟨m, hm, n, hn, equalX⟩ := integralX356  obtain ⟨p, hp, q, hq, equalY⟩ := integralY357  have natM := nat.omega.backward with hm358  have natN := nat.omega.backward with hn359  have natP := nat.omega.backward with hp360  have natQ := nat.omega.backward with hq361  have sumIn : add(m, p) ∈ ℕ := nat.omega.forward at add(m, p) with *362  have sumIn2 : add(n, q) ∈ ℕ := nat.omega.forward at add(n, q) with *363  unfold IntReal364  refine ⟨add(m, p), sumIn, add(n, q), sumIn2, ?_⟩365  rw [equalX, equalY, realNat.add, realNat.add]366  ring367368theorem IntReal.neg (x : Set)369  requires integral : IntReal(x)370  shows IntReal(-(x:R))371proof372  obtain ⟨m, hm, n, hn, equal⟩ := integral373  have natM := nat.omega.backward with hm374  have natN := nat.omega.backward with hn375  unfold IntReal376  refine ⟨n, hn, m, hm, ?_⟩377  rw equal378  ring379380theorem IntReal.sub (x y : Set)381  requires integralX : IntReal(x)382  requires integralY : IntReal(y)383  shows IntReal((x:R) - (y:R))384proof385  have realX := IntReal.real with integralX386  have realY := IntReal.real with integralY387  have negative := IntReal.neg with integralY388  have sum := IntReal.add with integralX, negative389  have same : (x:R) - (y:R) = (x:R) + -(y:R) by ring390  rw same391  exact sum392393theorem IntReal.mul (x y : Set)394  requires integralX : IntReal(x)395  requires integralY : IntReal(y)396  shows IntReal((x:R) * (y:R))397proof398  obtain ⟨m, hm, n, hn, equalX⟩ := integralX399  obtain ⟨p, hp, q, hq, equalY⟩ := integralY400  have natM := nat.omega.backward with hm401  have natN := nat.omega.backward with hn402  have natP := nat.omega.backward with hp403  have natQ := nat.omega.backward with hq404  have firstIn : add(mul(m, p), mul(n, q)) ∈ ℕ := nat.omega.forward at add(mul(m, p), mul(n, q)) with *405  have secondIn : add(mul(m, q), mul(n, p)) ∈ ℕ := nat.omega.forward at add(mul(m, q), mul(n, p)) with *406  unfold IntReal407  refine ⟨add(mul(m, p), mul(n, q)), firstIn, add(mul(m, q), mul(n, p)), secondIn, ?_⟩408  rw [equalX, equalY, realNat.add, realNat.add, realNat.mul, realNat.mul,409    realNat.mul, realNat.mul]410  ring411412theorem Div5.real (x : Set)413  requires divisible : Div5(x)414  shows x ∈ ℝ415proof416  obtain ⟨m, hm, n, hn, equal⟩ := divisible417  have natM := nat.omega.backward with hm418  have natN := nat.omega.backward with hn419  rw equal420  typecheck421422theorem Div5.zero423  shows Div5((0:R))424proof425  have zeroIn : 0 ∈ ℕ := nat.omega.forward at 0 with *426  unfold Div5427  refine ⟨0, zeroIn, 0, zeroIn, ?_⟩428  rw realNat.zero429  ring430431theorem Div5.of_eq (x y : Set)432  requires divisible : Div5(x)433  requires equal : y = x434  shows Div5(y)435proof436  rw equal437  exact divisible438439theorem Div5.add (x y : Set)440  requires divisibleX : Div5(x)441  requires divisibleY : Div5(y)442  shows Div5((x:R) + (y:R))443proof444  obtain ⟨m, hm, n, hn, equalX⟩ := divisibleX445  obtain ⟨p, hp, q, hq, equalY⟩ := divisibleY446  have natM := nat.omega.backward with hm447  have natN := nat.omega.backward with hn448  have natP := nat.omega.backward with hp449  have natQ := nat.omega.backward with hq450  have sumIn : add(m, p) ∈ ℕ := nat.omega.forward at add(m, p) with *451  have sumIn2 : add(n, q) ∈ ℕ := nat.omega.forward at add(n, q) with *452  unfold Div5453  refine ⟨add(m, p), sumIn, add(n, q), sumIn2, ?_⟩454  rw [equalX, equalY, realNat.add, realNat.add]455  ring456457theorem Div5.neg (x : Set)458  requires divisible : Div5(x)459  shows Div5(-(x:R))460proof461  obtain ⟨m, hm, n, hn, equal⟩ := divisible462  have natM := nat.omega.backward with hm463  have natN := nat.omega.backward with hn464  unfold Div5465  refine ⟨n, hn, m, hm, ?_⟩466  rw equal467  ring468469theorem Div5.sub (x y : Set)470  requires divisibleX : Div5(x)471  requires divisibleY : Div5(y)472  shows Div5((x:R) - (y:R))473proof474  have realX := Div5.real with divisibleX475  have realY := Div5.real with divisibleY476  have negative := Div5.neg with divisibleY477  have sum := Div5.add with divisibleX, negative478  have same : (x:R) - (y:R) = (x:R) + -(y:R) by ring479  rw same480  exact sum481482theorem Div5.mul_int (x y : Set)483  requires divisible : Div5(x)484  requires integral : IntReal(y)485  shows Div5((x:R) * (y:R))486proof487  obtain ⟨m, hm, n, hn, equalX⟩ := divisible488  obtain ⟨p, hp, q, hq, equalY⟩ := integral489  have natM := nat.omega.backward with hm490  have natN := nat.omega.backward with hn491  have natP := nat.omega.backward with hp492  have natQ := nat.omega.backward with hq493  have firstIn : add(mul(m, p), mul(n, q)) ∈ ℕ := nat.omega.forward at add(mul(m, p), mul(n, q)) with *494  have secondIn : add(mul(m, q), mul(n, p)) ∈ ℕ := nat.omega.forward at add(mul(m, q), mul(n, p)) with *495  unfold Div5496  refine ⟨add(mul(m, p), mul(n, q)), firstIn, add(mul(m, q), mul(n, p)), secondIn, ?_⟩497  rw [equalX, equalY, realNat.add, realNat.add, realNat.mul, realNat.mul,498    realNat.mul, realNat.mul]499  ring500501theorem Div5.five (x : Set)502  requires integral : IntReal(x)503  shows Div5(5 * (x:R))504proof505  obtain ⟨m, hm, n, hn, equal⟩ := integral506  have natM := nat.omega.backward with hm507  have natN := nat.omega.backward with hn508  unfold Div5509  refine ⟨m, hm, n, hn, ?_⟩510  rw equal511  ring512513-- A multiple of five that is three times an integer: the integer itself514-- is a multiple of five.515theorem Div5.of_three (x : Set)516  requires integral : IntReal(x)517  requires divisible : Div5(3 * (x:R))518  shows Div5(x)519proof520  have realX := IntReal.real with integral521  have two := IntReal.numeral at 2522  have doubled := Div5.mul_int with divisible, two523  have fived := Div5.five with integral524  have difference := Div5.sub with doubled, fived525  have same : (x:R) = 3 * (x:R) * 2 - 5 * (x:R) by ring526  exact Div5.of_eq with difference, same527528-- Neither 4 nor −4 is a multiple of five.529theorem Div5.not_four530  shows ¬Div5((4:R))531proof532  intro divisible533  obtain ⟨m, hm, n, hn, equal⟩ := divisible534  have natM := nat.omega.backward with hm535  have natN := nat.omega.backward with hn536  have cast : (realNat(add(4, mul(5, n))):R) = realNat(mul(5, m))537    have fourCast : (realNat(4):R) = (4:R)538      unfold realNumeral539      rfl540    have fiveCast : (realNat(5):R) = (5:R)541      unfold realNumeral542      rfl543    rw [realNat.add, realNat.mul, realNat.mul, fourCast, fiveCast]544    linarith545  have natural := realNat.injective with cast546  have cases := Less.trichotomy at m, n with natM, natN547  rcases cases with less | same | greater548  . arith549  . arith550  . arith551552theorem Div5.not_neg_four553  shows ¬Div5((0:R) - 4)554proof555  intro divisible556  obtain ⟨m, hm, n, hn, equal⟩ := divisible557  have natM := nat.omega.backward with hm558  have natN := nat.omega.backward with hn559  have cast : (realNat(add(4, mul(5, m))):R) = realNat(mul(5, n))560    have fourCast : (realNat(4):R) = (4:R)561      unfold realNumeral562      rfl563    have fiveCast : (realNat(5):R) = (5:R)564      unfold realNumeral565      rfl566    rw [realNat.add, realNat.mul, realNat.mul, fourCast, fiveCast]567    linarith568  have natural := realNat.injective with cast569  have cases := Less.trichotomy at m, n with natM, natN570  rcases cases with less | same | greater571  . arith572  . arith573  . arith574575-- The letter 3 differs from the others.576theorem letter.zero_ne_three577  shows 0 ≠ 3578proof579  intro equal580  arith581582theorem letter.one_ne_three583  shows 1 ≠ 3584proof585  intro equal586  arith587588theorem letter.two_ne_three589  shows 2 ≠ 3590proof591  intro equal592  arith593594theorem letter.three_ne_zero595  shows 3 ≠ 0596proof597  intro equal598  arith599600theorem letter.three_ne_one601  shows 3 ≠ 1602proof603  intro equal604  arith605606theorem letter.three_ne_two607  shows 3 ≠ 2608proof609  intro equal610  arith611612-- The residues modulo 5 forced on the integer vector (a, b, c) by the613-- first letter h of the word: after a rotation about the x-axis the first614-- coordinate is a multiple of five and the third is 3b or 2b modulo 5;615-- after one about the z-axis the third coordinate is a multiple of five616-- and the second is 3a or 2a modulo 5.617predicate HeadRelation (h a b c : Set) :=618  (h = 0 → Div5(a) ∧ Div5((c:R) - 3 * (b:R))) ∧619  (h = 1 → Div5(a) ∧ Div5((c:R) - 2 * (b:R))) ∧620  (h = 2 → Div5(c) ∧ Div5((b:R) - 3 * (a:R))) ∧621  (h = 3 → Div5(c) ∧ Div5((b:R) - 2 * (a:R)))622623theorem HeadRelation.zero (a b c : Set)624  requires first : Div5(a)625  requires third : Div5((c:R) - 3 * (b:R))626  shows HeadRelation(0, a, b, c)627proof628  unfold HeadRelation629  constructor630  . intro equal631    exact ⟨first, third⟩632  . constructor633    . intro equal634      exfalso635      exact index.zero_ne_one with equal636    . constructor637      . intro equal638        exfalso639        exact index.zero_ne_two with equal640      . intro equal641        exfalso642        exact letter.zero_ne_three with equal643644theorem HeadRelation.one (a b c : Set)645  requires first : Div5(a)646  requires third : Div5((c:R) - 2 * (b:R))647  shows HeadRelation(1, a, b, c)648proof649  unfold HeadRelation650  constructor651  . intro equal652    exfalso653    exact index.one_ne_zero with equal654  . constructor655    . intro equal656      exact ⟨first, third⟩657    . constructor658      . intro equal659        exfalso660        exact index.one_ne_two with equal661      . intro equal662        exfalso663        exact letter.one_ne_three with equal664665theorem HeadRelation.two (a b c : Set)666  requires third : Div5(c)667  requires second : Div5((b:R) - 3 * (a:R))668  shows HeadRelation(2, a, b, c)669proof670  unfold HeadRelation671  constructor672  . intro equal673    exfalso674    exact index.two_ne_zero with equal675  . constructor676    . intro equal677      exfalso678      exact index.two_ne_one with equal679    . constructor680      . intro equal681        exact ⟨third, second⟩682      . intro equal683        exfalso684        exact letter.two_ne_three with equal685686theorem HeadRelation.three (a b c : Set)687  requires third : Div5(c)688  requires second : Div5((b:R) - 2 * (a:R))689  shows HeadRelation(3, a, b, c)690proof691  unfold HeadRelation692  constructor693  . intro equal694    exfalso695    exact letter.three_ne_zero with equal696  . constructor697    . intro equal698      exfalso699      exact letter.three_ne_one with equal700    . constructor701      . intro equal702        exfalso703        exact letter.three_ne_two with equal704      . intro equal705        exact ⟨third, second⟩706707-- One step of Swierczkowski's argument for each generator: from an708-- integer vector (a, b, c) with b not a multiple of five, whose residues709-- are those of a word with first letter h, the vector after the letter710-- ℓ ≠ h⁻¹ again has a middle coordinate that is not a multiple of five.711theorem step.rotA (a b c h : Set)712  requires intA : IntReal(a)713  requires intB : IntReal(b)714  requires intC : IntReal(c)715  requires nonzero : ¬Div5(b)716  requires relation : HeadRelation(h, a, b, c)717  requires letter : h ∈ 4718  requires reduced : h ≠ 1719  shows IntReal(5 * (a:R)) ∧ IntReal(3 * (b:R) - 4 * (c:R)) ∧720    IntReal(4 * (b:R) + 3 * (c:R)) ∧ ¬Div5(3 * (b:R) - 4 * (c:R)) ∧721    HeadRelation(0, 5 * (a:R), 3 * (b:R) - 4 * (c:R), 4 * (b:R) + 3 * (c:R))722proof723  have realA := IntReal.real with intA724  have realB := IntReal.real with intB725  have realC := IntReal.real with intC726  have two := IntReal.numeral at 2727  have three := IntReal.numeral at 3728  have four := IntReal.numeral at 4729  have five := IntReal.numeral at 5730  have eight := IntReal.numeral at 8731  have int5a := IntReal.mul with five, intA732  have int3b := IntReal.mul with three, intB733  have int4c := IntReal.mul with four, intC734  have int4b := IntReal.mul with four, intB735  have int3c := IntReal.mul with three, intC736  have int2b := IntReal.mul with two, intB737  have newB := IntReal.sub with int3b, int4c738  have newC := IntReal.add with int4b, int3c739  have newRelation : HeadRelation(0, 5 * (a:R), 3 * (b:R) - 4 * (c:R), 4 * (b:R) + 3 * (c:R))740    have divA := Div5.five with intA741    have combo := IntReal.sub with int3c, intB742    have divCombo := Div5.five with combo743    have same : (4 * (b:R) + 3 * (c:R)) - 3 * (3 * (b:R) - 4 * (c:R)) = 5 * (3 * (c:R) - (b:R)) by ring744    have divC := Div5.of_eq with divCombo, same745    exact HeadRelation.zero with divA, divC746  have newNonzero : ¬Div5(3 * (b:R) - 4 * (c:R))747    intro divisible748    obtain ⟨rel0, rel1, rel2, rel3⟩ := relation749    have alternatives := letter.cases with letter750    rcases alternatives with at0 | at1 | at2 | at3751    . obtain ⟨divA, divCB⟩ := rel0 with at0752      have t1 := Div5.mul_int with divCB, four753      have t2 := Div5.five with int2b754      have partial := Div5.add with divisible, t1755      have sum := Div5.add with partial, t2756      have same : (b:R) = (3 * (b:R) - 4 * (c:R)) + ((c:R) - 3 * (b:R)) * 4 + 5 * (2 * (b:R)) by ring757      exact nonzero with (Div5.of_eq with sum, same)758    . exact reduced with at1759    . obtain ⟨divC, divBA⟩ := rel2 with at2760      have t1 := Div5.mul_int with divisible, two761      have t2 := Div5.mul_int with divC, eight762      have t3 := Div5.five with intB763      have partial := Div5.add with t1, t2764      have combo := Div5.sub with partial, t3765      have same : (b:R) = (3 * (b:R) - 4 * (c:R)) * 2 + (c:R) * 8 - 5 * (b:R) by ring766      exact nonzero with (Div5.of_eq with combo, same)767    . obtain ⟨divC, divBA⟩ := rel3 with at3768      have t1 := Div5.mul_int with divisible, two769      have t2 := Div5.mul_int with divC, eight770      have t3 := Div5.five with intB771      have partial := Div5.add with t1, t2772      have combo := Div5.sub with partial, t3773      have same : (b:R) = (3 * (b:R) - 4 * (c:R)) * 2 + (c:R) * 8 - 5 * (b:R) by ring774      exact nonzero with (Div5.of_eq with combo, same)775  exact ⟨int5a, newB, newC, newNonzero, newRelation⟩776777theorem step.rotA_transpose (a b c h : Set)778  requires intA : IntReal(a)779  requires intB : IntReal(b)780  requires intC : IntReal(c)781  requires nonzero : ¬Div5(b)782  requires relation : HeadRelation(h, a, b, c)783  requires letter : h ∈ 4784  requires reduced : h ≠ 0785  shows IntReal(5 * (a:R)) ∧ IntReal(3 * (b:R) + 4 * (c:R)) ∧786    IntReal(3 * (c:R) - 4 * (b:R)) ∧ ¬Div5(3 * (b:R) + 4 * (c:R)) ∧787    HeadRelation(1, 5 * (a:R), 3 * (b:R) + 4 * (c:R), 3 * (c:R) - 4 * (b:R))788proof789  have realA := IntReal.real with intA790  have realB := IntReal.real with intB791  have realC := IntReal.real with intC792  have two := IntReal.numeral at 2793  have three := IntReal.numeral at 3794  have four := IntReal.numeral at 4795  have five := IntReal.numeral at 5796  have eight := IntReal.numeral at 8797  have int5a := IntReal.mul with five, intA798  have int3b := IntReal.mul with three, intB799  have int4c := IntReal.mul with four, intC800  have int4b := IntReal.mul with four, intB801  have int3c := IntReal.mul with three, intC802  have int2b := IntReal.mul with two, intB803  have newB := IntReal.add with int3b, int4c804  have newC := IntReal.sub with int3c, int4b805  have newRelation : HeadRelation(1, 5 * (a:R), 3 * (b:R) + 4 * (c:R), 3 * (c:R) - 4 * (b:R))806    have divA := Div5.five with intA807    have negative := IntReal.neg with int2b808    have combo := IntReal.sub with negative, intC809    have divCombo := Div5.five with combo810    have same : (3 * (c:R) - 4 * (b:R)) - 2 * (3 * (b:R) + 4 * (c:R)) = 5 * (-(2 * (b:R)) - (c:R)) by ring811    have divC := Div5.of_eq with divCombo, same812    exact HeadRelation.one with divA, divC813  have newNonzero : ¬Div5(3 * (b:R) + 4 * (c:R))814    intro divisible815    obtain ⟨rel0, rel1, rel2, rel3⟩ := relation816    have alternatives := letter.cases with letter817    rcases alternatives with at0 | at1 | at2 | at3818    . exact reduced with at0819    . obtain ⟨divA, divCB⟩ := rel1 with at1820      have t1 := Div5.mul_int with divCB, four821      have t2 := Div5.five with int2b822      have partial := Div5.sub with divisible, t1823      have difference := Div5.sub with partial, t2824      have same : (b:R) = (3 * (b:R) + 4 * (c:R)) - ((c:R) - 2 * (b:R)) * 4 - 5 * (2 * (b:R)) by ring825      exact nonzero with (Div5.of_eq with difference, same)826    . obtain ⟨divC, divBA⟩ := rel2 with at2827      have t1 := Div5.mul_int with divisible, two828      have t2 := Div5.mul_int with divC, eight829      have t3 := Div5.five with intB830      have partial := Div5.sub with t1, t2831      have combo := Div5.sub with partial, t3832      have same : (b:R) = (3 * (b:R) + 4 * (c:R)) * 2 - (c:R) * 8 - 5 * (b:R) by ring833      exact nonzero with (Div5.of_eq with combo, same)834    . obtain ⟨divC, divBA⟩ := rel3 with at3835      have t1 := Div5.mul_int with divisible, two836      have t2 := Div5.mul_int with divC, eight837      have t3 := Div5.five with intB838      have partial := Div5.sub with t1, t2839      have combo := Div5.sub with partial, t3840      have same : (b:R) = (3 * (b:R) + 4 * (c:R)) * 2 - (c:R) * 8 - 5 * (b:R) by ring841      exact nonzero with (Div5.of_eq with combo, same)842  exact ⟨int5a, newB, newC, newNonzero, newRelation⟩843844theorem step.rotB (a b c h : Set)845  requires intA : IntReal(a)846  requires intB : IntReal(b)847  requires intC : IntReal(c)848  requires nonzero : ¬Div5(b)849  requires relation : HeadRelation(h, a, b, c)850  requires letter : h ∈ 4851  requires reduced : h ≠ 3852  shows IntReal(3 * (a:R) - 4 * (b:R)) ∧ IntReal(4 * (a:R) + 3 * (b:R)) ∧853    IntReal(5 * (c:R)) ∧ ¬Div5(4 * (a:R) + 3 * (b:R)) ∧854    HeadRelation(2, 3 * (a:R) - 4 * (b:R), 4 * (a:R) + 3 * (b:R), 5 * (c:R))855proof856  have realA := IntReal.real with intA857  have realB := IntReal.real with intB858  have realC := IntReal.real with intC859  have two := IntReal.numeral at 2860  have three := IntReal.numeral at 3861  have four := IntReal.numeral at 4862  have five := IntReal.numeral at 5863  have int5c := IntReal.mul with five, intC864  have int3a := IntReal.mul with three, intA865  have int4b := IntReal.mul with four, intB866  have int4a := IntReal.mul with four, intA867  have int3b := IntReal.mul with three, intB868  have int2b := IntReal.mul with two, intB869  have newA := IntReal.sub with int3a, int4b870  have newB := IntReal.add with int4a, int3b871  have newRelation : HeadRelation(2, 3 * (a:R) - 4 * (b:R), 4 * (a:R) + 3 * (b:R), 5 * (c:R))872    have divC := Div5.five with intC873    have combo := IntReal.sub with int3b, intA874    have divCombo := Div5.five with combo875    have same : (4 * (a:R) + 3 * (b:R)) - 3 * (3 * (a:R) - 4 * (b:R)) = 5 * (3 * (b:R) - (a:R)) by ring876    have divB := Div5.of_eq with divCombo, same877    exact HeadRelation.two with divC, divB878  have newNonzero : ¬Div5(4 * (a:R) + 3 * (b:R))879    intro divisible880    obtain ⟨rel0, rel1, rel2, rel3⟩ := relation881    have alternatives := letter.cases with letter882    rcases alternatives with at0 | at1 | at2 | at3883    . obtain ⟨divA, divCB⟩ := rel0 with at0884      have t1 := Div5.mul_int with divA, four885      have difference := Div5.sub with divisible, t1886      have same : 3 * (b:R) = (4 * (a:R) + 3 * (b:R)) - (a:R) * 4 by ring887      have triple := Div5.of_eq with difference, same888      exact nonzero with (Div5.of_three with intB, triple)889    . obtain ⟨divA, divCB⟩ := rel1 with at1890      have t1 := Div5.mul_int with divA, four891      have difference := Div5.sub with divisible, t1892      have same : 3 * (b:R) = (4 * (a:R) + 3 * (b:R)) - (a:R) * 4 by ring893      have triple := Div5.of_eq with difference, same894      exact nonzero with (Div5.of_three with intB, triple)895    . obtain ⟨divC, divBA⟩ := rel2 with at2896      have t1 := Div5.mul_int with divisible, three897      have t2 := Div5.mul_int with divBA, four898      have t3 := Div5.five with int2b899      have partial := Div5.add with t1, t2900      have combo := Div5.sub with partial, t3901      have same : 3 * (b:R) = (4 * (a:R) + 3 * (b:R)) * 3 + ((b:R) - 3 * (a:R)) * 4 - 5 * (2 * (b:R)) by ring902      have triple := Div5.of_eq with combo, same903      exact nonzero with (Div5.of_three with intB, triple)904    . exact reduced with at3905  exact ⟨newA, newB, int5c, newNonzero, newRelation⟩906907theorem step.rotB_transpose (a b c h : Set)908  requires intA : IntReal(a)909  requires intB : IntReal(b)910  requires intC : IntReal(c)911  requires nonzero : ¬Div5(b)912  requires relation : HeadRelation(h, a, b, c)913  requires letter : h ∈ 4914  requires reduced : h ≠ 2915  shows IntReal(3 * (a:R) + 4 * (b:R)) ∧ IntReal(3 * (b:R) - 4 * (a:R)) ∧916    IntReal(5 * (c:R)) ∧ ¬Div5(3 * (b:R) - 4 * (a:R)) ∧917    HeadRelation(3, 3 * (a:R) + 4 * (b:R), 3 * (b:R) - 4 * (a:R), 5 * (c:R))918proof919  have realA := IntReal.real with intA920  have realB := IntReal.real with intB921  have realC := IntReal.real with intC922  have two := IntReal.numeral at 2923  have three := IntReal.numeral at 3924  have four := IntReal.numeral at 4925  have five := IntReal.numeral at 5926  have six := IntReal.numeral at 6927  have int5c := IntReal.mul with five, intC928  have int3a := IntReal.mul with three, intA929  have int4b := IntReal.mul with four, intB930  have int4a := IntReal.mul with four, intA931  have int3b := IntReal.mul with three, intB932  have int2a := IntReal.mul with two, intA933  have newA := IntReal.add with int3a, int4b934  have newB := IntReal.sub with int3b, int4a935  have newRelation : HeadRelation(3, 3 * (a:R) + 4 * (b:R), 3 * (b:R) - 4 * (a:R), 5 * (c:R))936    have divC := Div5.five with intC937    have negative := IntReal.neg with int2a938    have combo := IntReal.sub with negative, intB939    have divCombo := Div5.five with combo940    have same : (3 * (b:R) - 4 * (a:R)) - 2 * (3 * (a:R) + 4 * (b:R)) = 5 * (-(2 * (a:R)) - (b:R)) by ring941    have divB := Div5.of_eq with divCombo, same942    exact HeadRelation.three with divC, divB943  have newNonzero : ¬Div5(3 * (b:R) - 4 * (a:R))944    intro divisible945    obtain ⟨rel0, rel1, rel2, rel3⟩ := relation946    have alternatives := letter.cases with letter947    rcases alternatives with at0 | at1 | at2 | at3948    . obtain ⟨divA, divCB⟩ := rel0 with at0949      have t1 := Div5.mul_int with divA, four950      have sum := Div5.add with divisible, t1951      have same : 3 * (b:R) = (3 * (b:R) - 4 * (a:R)) + (a:R) * 4 by ring952      have triple := Div5.of_eq with sum, same953      exact nonzero with (Div5.of_three with intB, triple)954    . obtain ⟨divA, divCB⟩ := rel1 with at1955      have t1 := Div5.mul_int with divA, four956      have sum := Div5.add with divisible, t1957      have same : 3 * (b:R) = (3 * (b:R) - 4 * (a:R)) + (a:R) * 4 by ring958      have triple := Div5.of_eq with sum, same959      exact nonzero with (Div5.of_three with intB, triple)960    . exact reduced with at2961    . obtain ⟨divC, divBA⟩ := rel3 with at3962      have t1 := Div5.mul_int with divisible, three963      have t2 := Div5.mul_int with divBA, six964      have combo := Div5.sub with t1, t2965      have same : 3 * (b:R) = (3 * (b:R) - 4 * (a:R)) * 3 - ((b:R) - 2 * (a:R)) * 6 by ring966      have triple := Div5.of_eq with combo, same967      exact nonzero with (Div5.of_three with intB, triple)968  exact ⟨newA, newB, int5c, newNonzero, newRelation⟩969970-- The basis vectors of ℝ³.971defgraph basis (j : Set) (i ∈ 3) : ℝ :=972  singleValue(Ring.carrier(realRing), Ring.zero(realRing), Ring.one(realRing), j, i)973requires index : j ∈ 3974proof975  have comm := realRing.comm_ring976  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *977  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *978  have closed := singleValue.closed at Ring.carrier(realRing), Ring.zero(realRing),979    Ring.one(realRing), j, i with *980  rw ← realRing.carrierOf981  exact closed982983instance basis.vector (j : Set)984  requires index : j ∈ 3985  shows basis(j) : 3 → ℝ986proof987  exact basis.function with index988989theorem basis.same (j : Set)990  requires index : j ∈ 3991  shows basis(j)(j) = (1:R)992proof993  have comm := realRing.comm_ring994  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *995  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *996  have same : j = j by rfl997  have value := basis.value at j, j with *998  have selected := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),999    Ring.one(realRing), j, j with zeroIn, oneIn, same1000  rw [value, selected, realRing.one_value]1001  rfl10021003theorem basis.other (i j : Set)1004  requires row : i ∈ 31005  requires index : j ∈ 31006  requires different : i ≠ j1007  shows basis(j)(i) = (0:R)1008proof1009  have comm := realRing.comm_ring1010  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *1011  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *1012  have value := basis.value at j, i with *1013  have selected := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),1014    Ring.one(realRing), j, i with zeroIn, oneIn, different1015  rw [value, selected, realRing.zero_value]1016  rfl10171018-- The four letters, as Algebra/Group/Words states them.1019theorem letterIn.zero1020  shows 0 ∈ 41021proof1022  exact letter.zero_mem10231024theorem letterIn.one1025  shows 1 ∈ 41026proof1027  exact letter.one_mem10281029theorem letterIn.two1030  shows 2 ∈ 41031proof1032  exact letter.two_mem10331034theorem letterIn.three1035  shows 3 ∈ 41036proof1037  exact letter.three_mem10381039-- The scaled coordinates along a word: the empty word gives the start1040-- vector, and a letter in front acts by five times its matrix.1041theorem coordinate.nil (v i : Set)1042  requires vector : v : 3 → ℝ1043  requires index : i ∈ 31044  shows coordinate([], v, i) = (v(i):R)1045proof1046  have component := vector.component_real at v, i with *1047  rw [coordinate.value, fivePow.nil, wordRotation.nil, matrixVector.one]1048  ring10491050theorem coordinate.cons (ℓ : Set) (rest : List(4)) (v i : Set)1051  requires letter : ℓ ∈ 41052  requires vector : v : 3 → ℝ1053  requires index : i ∈ 31054  shows coordinate(ℓ :: rest, v, i) =1055    (fivePow(rest):R) * (5 * ((letterMatrix(ℓ) · (wordRotation(rest) · v))(i):R))1056proof1057  have matrix := letterMatrix.matrix with letter1058  have inner := matrixVector.vector at wordRotation(rest), v with *1059  have outer := matrixVector.vector at letterMatrix(ℓ), wordRotation(rest) · v with *1060  have component := vector.component_real at letterMatrix(ℓ) · (wordRotation(rest) · v), i with *1061  have scale := fivePow.real at rest1062  have law := matrixVector.mul at letterMatrix(ℓ), wordRotation(rest), v with *1063  rw [coordinate.value, fivePow.cons, wordRotation.cons, law]1064  ring10651066theorem coordinate.consA (rest : List(4)) (v : Set)1067  requires vector : v : 3 → ℝ1068  shows coordinate(0 :: rest, v, 0) = 5 * (coordinate(rest, v, 0):R) ∧1069    coordinate(0 :: rest, v, 1) = 3 * (coordinate(rest, v, 1):R) - 4 * (coordinate(rest, v, 2):R) ∧1070    coordinate(0 :: rest, v, 2) = 4 * (coordinate(rest, v, 1):R) + 3 * (coordinate(rest, v, 2):R)1071proof1072  have letter := letterIn.zero1073  have inner := matrixVector.vector at wordRotation(rest), v with *1074  obtain ⟨f0, f1, f2⟩ := rotA.five_action at wordRotation(rest) · v with inner1075  have c0 := coordinate.cons at 0, rest, v, 0 with *1076  have c1 := coordinate.cons at 0, rest, v, 1 with *1077  have c2 := coordinate.cons at 0, rest, v, 2 with *1078  have u0 := vector.component_real at wordRotation(rest) · v, 0 with *1079  have u1 := vector.component_real at wordRotation(rest) · v, 1 with *1080  have u2 := vector.component_real at wordRotation(rest) · v, 2 with *1081  have scale := fivePow.real at rest1082  constructor1083  . rw [c0, letterMatrix.zero, f0, coordinate.value]1084    ring1085  . constructor1086    . rw [c1, letterMatrix.zero, f1, coordinate.value, coordinate.value]1087      ring1088    . rw [c2, letterMatrix.zero, f2, coordinate.value, coordinate.value]1089      ring10901091theorem coordinate.consAT (rest : List(4)) (v : Set)1092  requires vector : v : 3 → ℝ1093  shows coordinate(1 :: rest, v, 0) = 5 * (coordinate(rest, v, 0):R) ∧1094    coordinate(1 :: rest, v, 1) = 3 * (coordinate(rest, v, 1):R) + 4 * (coordinate(rest, v, 2):R) ∧1095    coordinate(1 :: rest, v, 2) = 3 * (coordinate(rest, v, 2):R) - 4 * (coordinate(rest, v, 1):R)1096proof1097  have letter := letterIn.one1098  have inner := matrixVector.vector at wordRotation(rest), v with *1099  obtain ⟨f0, f1, f2⟩ := rotA.transpose_five_action at wordRotation(rest) · v with inner1100  have c0 := coordinate.cons at 1, rest, v, 0 with *1101  have c1 := coordinate.cons at 1, rest, v, 1 with *1102  have c2 := coordinate.cons at 1, rest, v, 2 with *1103  have u0 := vector.component_real at wordRotation(rest) · v, 0 with *1104  have u1 := vector.component_real at wordRotation(rest) · v, 1 with *1105  have u2 := vector.component_real at wordRotation(rest) · v, 2 with *1106  have scale := fivePow.real at rest1107  constructor1108  . rw [c0, letterMatrix.one, f0, coordinate.value]1109    ring1110  . constructor1111    . rw [c1, letterMatrix.one, f1, coordinate.value, coordinate.value]1112      ring1113    . rw [c2, letterMatrix.one, f2, coordinate.value, coordinate.value]1114      ring11151116theorem coordinate.consB (rest : List(4)) (v : Set)1117  requires vector : v : 3 → ℝ1118  shows coordinate(2 :: rest, v, 0) = 3 * (coordinate(rest, v, 0):R) - 4 * (coordinate(rest, v, 1):R) ∧1119    coordinate(2 :: rest, v, 1) = 4 * (coordinate(rest, v, 0):R) + 3 * (coordinate(rest, v, 1):R) ∧1120    coordinate(2 :: rest, v, 2) = 5 * (coordinate(rest, v, 2):R)1121proof1122  have letter := letterIn.two1123  have inner := matrixVector.vector at wordRotation(rest), v with *1124  obtain ⟨f0, f1, f2⟩ := rotB.five_action at wordRotation(rest) · v with inner1125  have c0 := coordinate.cons at 2, rest, v, 0 with *1126  have c1 := coordinate.cons at 2, rest, v, 1 with *1127  have c2 := coordinate.cons at 2, rest, v, 2 with *1128  have u0 := vector.component_real at wordRotation(rest) · v, 0 with *1129  have u1 := vector.component_real at wordRotation(rest) · v, 1 with *1130  have u2 := vector.component_real at wordRotation(rest) · v, 2 with *1131  have scale := fivePow.real at rest1132  constructor1133  . rw [c0, letterMatrix.two, f0, coordinate.value, coordinate.value]1134    ring1135  . constructor1136    . rw [c1, letterMatrix.two, f1, coordinate.value, coordinate.value]1137      ring1138    . rw [c2, letterMatrix.two, f2, coordinate.value]1139      ring11401141theorem coordinate.consBT (rest : List(4)) (v : Set)1142  requires vector : v : 3 → ℝ1143  shows coordinate(3 :: rest, v, 0) = 3 * (coordinate(rest, v, 0):R) + 4 * (coordinate(rest, v, 1):R) ∧1144    coordinate(3 :: rest, v, 1) = 3 * (coordinate(rest, v, 1):R) - 4 * (coordinate(rest, v, 0):R) ∧1145    coordinate(3 :: rest, v, 2) = 5 * (coordinate(rest, v, 2):R)1146proof1147  have letter := letterIn.three1148  have inner := matrixVector.vector at wordRotation(rest), v with *1149  obtain ⟨f0, f1, f2⟩ := rotB.transpose_five_action at wordRotation(rest) · v with inner1150  have c0 := coordinate.cons at 3, rest, v, 0 with *1151  have c1 := coordinate.cons at 3, rest, v, 1 with *1152  have c2 := coordinate.cons at 3, rest, v, 2 with *1153  have u0 := vector.component_real at wordRotation(rest) · v, 0 with *1154  have u1 := vector.component_real at wordRotation(rest) · v, 1 with *1155  have u2 := vector.component_real at wordRotation(rest) · v, 2 with *1156  have scale := fivePow.real at rest1157  constructor1158  . rw [c0, letterMatrix.three, f0, coordinate.value, coordinate.value]1159    ring1160  . constructor1161    . rw [c1, letterMatrix.three, f1, coordinate.value, coordinate.value]1162      ring1163    . rw [c2, letterMatrix.three, f2, coordinate.value]1164      ring11651166-- Swierczkowski's invariant for the word ℓ :: rest from the start vector1167-- v: the scaled coordinates are integers, the middle one is not a1168-- multiple of five, and the residues are those forced by the letter ℓ.1169predicate Swierczkowski (ℓ rest v : Set) :=1170  IntReal(coordinate(ℓ :: rest, v, 0)) ∧ IntReal(coordinate(ℓ :: rest, v, 1)) ∧1171  IntReal(coordinate(ℓ :: rest, v, 2)) ∧ ¬Div5(coordinate(ℓ :: rest, v, 1)) ∧1172  HeadRelation(ℓ, coordinate(ℓ :: rest, v, 0), coordinate(ℓ :: rest, v, 1),1173    coordinate(ℓ :: rest, v, 2))11741175theorem Swierczkowski.step (ℓ h : Set) (rest : List(4)) (v : Set)1176  requires letterL : ℓ ∈ 41177  requires letterH : h ∈ 41178  requires reduced : h ≠ inverseLetter(ℓ)1179  requires vector : v : 3 → ℝ1180  requires invariant : Swierczkowski(h, rest, v)1181  shows Swierczkowski(ℓ, h :: rest, v)1182proof1183  obtain ⟨intA, intB, intC, nonzero, relation⟩ := invariant1184  have alternatives := letter.cases with letterL1185  rcases alternatives with at0 | at1 | at2 | at31186  . rw [at0, inverseLetter.zero] at reduced1187    rw at01188    obtain ⟨c0, c1, c2⟩ := coordinate.consA at h :: rest, v with vector1189    obtain ⟨newA, newB, newC, newNonzero, newRelation⟩ := step.rotA with intA, intB,1190      intC, nonzero, relation, letterH, reduced1191    unfold Swierczkowski1192    rw [c0, c1, c2]1193    exact ⟨newA, newB, newC, newNonzero, newRelation⟩1194  . rw [at1, inverseLetter.one] at reduced1195    rw at11196    obtain ⟨c0, c1, c2⟩ := coordinate.consAT at h :: rest, v with vector1197    obtain ⟨newA, newB, newC, newNonzero, newRelation⟩ := step.rotA_transpose with intA,1198      intB, intC, nonzero, relation, letterH, reduced1199    unfold Swierczkowski1200    rw [c0, c1, c2]1201    exact ⟨newA, newB, newC, newNonzero, newRelation⟩1202  . rw [at2, inverseLetter.two] at reduced1203    rw at21204    obtain ⟨c0, c1, c2⟩ := coordinate.consB at h :: rest, v with vector1205    obtain ⟨newA, newB, newC, newNonzero, newRelation⟩ := step.rotB with intA, intB,1206      intC, nonzero, relation, letterH, reduced1207    unfold Swierczkowski1208    rw [c0, c1, c2]1209    exact ⟨newA, newB, newC, newNonzero, newRelation⟩1210  . rw [at3, inverseLetter.three] at reduced1211    rw at31212    obtain ⟨c0, c1, c2⟩ := coordinate.consBT at h :: rest, v with vector1213    obtain ⟨newA, newB, newC, newNonzero, newRelation⟩ := step.rotB_transpose with intA,1214      intB, intC, nonzero, relation, letterH, reduced1215    unfold Swierczkowski1216    rw [c0, c1, c2]1217    exact ⟨newA, newB, newC, newNonzero, newRelation⟩12181219-- The one-letter words: b and b⁻¹ from (1, 0, 0), a and a⁻¹ from (0, 0, 1).1220theorem Swierczkowski.base_b1221  shows Swierczkowski(2, [], basis(0))1222proof1223  have vector := basis.vector at 0 with *1224  have e0 := basis.same at 0 with *1225  have e1 := basis.other at 1, 0 with index.one_mem, index.zero_mem, index.one_ne_zero1226  have e2 := basis.other at 2, 0 with index.two_mem, index.zero_mem, index.two_ne_zero1227  obtain ⟨c0, c1, c2⟩ := coordinate.consB at [], basis(0) with vector1228  have n0 := coordinate.nil at basis(0), 0 with *1229  have n1 := coordinate.nil at basis(0), 1 with *1230  have n2 := coordinate.nil at basis(0), 2 with *1231  have value0 : coordinate(2 :: [], basis(0), 0) = (3:R)1232    rw [c0, n0, n1, e0, e1]1233    ring1234  have value1 : coordinate(2 :: [], basis(0), 1) = (4:R)1235    rw [c1, n0, n1, e0, e1]1236    ring1237  have value2 : coordinate(2 :: [], basis(0), 2) = (0:R)1238    rw [c2, n2, e2]1239    ring1240  have three := IntReal.numeral at 31241  have four := IntReal.numeral at 41242  have zero := IntReal.zero1243  have one := IntReal.one1244  have negative := IntReal.sub with zero, one1245  have multiple := Div5.five with negative1246  have residue : Div5((4:R) - 3 * (3:R))1247    have same : (4:R) - 3 * (3:R) = 5 * ((0:R) - (1:R)) by ring1248    rw same1249    exact multiple1250  have relation := HeadRelation.two at (3:R), (4:R), (0:R) with Div5.zero, residue1251  unfold Swierczkowski1252  rw [value0, value1, value2]1253  exact ⟨three, four, zero, Div5.not_four, relation⟩12541255theorem Swierczkowski.base_bt1256  shows Swierczkowski(3, [], basis(0))1257proof1258  have vector := basis.vector at 0 with *1259  have e0 := basis.same at 0 with *1260  have e1 := basis.other at 1, 0 with index.one_mem, index.zero_mem, index.one_ne_zero1261  have e2 := basis.other at 2, 0 with index.two_mem, index.zero_mem, index.two_ne_zero1262  obtain ⟨c0, c1, c2⟩ := coordinate.consBT at [], basis(0) with vector1263  have n0 := coordinate.nil at basis(0), 0 with *1264  have n1 := coordinate.nil at basis(0), 1 with *1265  have n2 := coordinate.nil at basis(0), 2 with *1266  have value0 : coordinate(3 :: [], basis(0), 0) = (3:R)1267    rw [c0, n0, n1, e0, e1]1268    ring1269  have value1 : coordinate(3 :: [], basis(0), 1) = (0:R) - 41270    rw [c1, n0, n1, e0, e1]1271    ring1272  have value2 : coordinate(3 :: [], basis(0), 2) = (0:R)1273    rw [c2, n2, e2]1274    ring1275  have three := IntReal.numeral at 31276  have four := IntReal.numeral at 41277  have zero := IntReal.zero1278  have two := IntReal.numeral at 21279  have negativeFour := IntReal.sub with zero, four1280  have negativeTwo := IntReal.sub with zero, two1281  have multiple := Div5.five with negativeTwo1282  have residue : Div5(((0:R) - 4) - 2 * (3:R))1283    have same : ((0:R) - 4) - 2 * (3:R) = 5 * ((0:R) - (2:R)) by ring1284    rw same1285    exact multiple1286  have relation := HeadRelation.three at (3:R), (0:R) - 4, (0:R) with Div5.zero, residue1287  unfold Swierczkowski1288  rw [value0, value1, value2]1289  exact ⟨three, negativeFour, zero, Div5.not_neg_four, relation⟩12901291theorem Swierczkowski.base_a1292  shows Swierczkowski(0, [], basis(2))1293proof1294  have vector := basis.vector at 2 with *1295  have e0 := basis.other at 0, 2 with index.zero_mem, index.two_mem, index.zero_ne_two1296  have e1 := basis.other at 1, 2 with index.one_mem, index.two_mem, index.one_ne_two1297  have e2 := basis.same at 2 with *1298  obtain ⟨c0, c1, c2⟩ := coordinate.consA at [], basis(2) with vector1299  have n0 := coordinate.nil at basis(2), 0 with *1300  have n1 := coordinate.nil at basis(2), 1 with *1301  have n2 := coordinate.nil at basis(2), 2 with *1302  have value0 : coordinate(0 :: [], basis(2), 0) = (0:R)1303    rw [c0, n0, e0]1304    ring1305  have value1 : coordinate(0 :: [], basis(2), 1) = (0:R) - 41306    rw [c1, n1, n2, e1, e2]1307    ring1308  have value2 : coordinate(0 :: [], basis(2), 2) = (3:R)1309    rw [c2, n1, n2, e1, e2]1310    ring1311  have three := IntReal.numeral at 31312  have four := IntReal.numeral at 41313  have zero := IntReal.zero1314  have negativeFour := IntReal.sub with zero, four1315  have multiple := Div5.five with three1316  have residue : Div5((3:R) - 3 * ((0:R) - 4))1317    have same : (3:R) - 3 * ((0:R) - 4) = 5 * (3:R) by ring1318    rw same1319    exact multiple1320  have relation := HeadRelation.zero at (0:R), (0:R) - 4, (3:R) with Div5.zero, residue1321  unfold Swierczkowski1322  rw [value0, value1, value2]1323  exact ⟨zero, negativeFour, three, Div5.not_neg_four, relation⟩13241325theorem Swierczkowski.base_at1326  shows Swierczkowski(1, [], basis(2))1327proof1328  have vector := basis.vector at 2 with *1329  have e0 := basis.other at 0, 2 with index.zero_mem, index.two_mem, index.zero_ne_two1330  have e1 := basis.other at 1, 2 with index.one_mem, index.two_mem, index.one_ne_two1331  have e2 := basis.same at 2 with *1332  obtain ⟨c0, c1, c2⟩ := coordinate.consAT at [], basis(2) with vector1333  have n0 := coordinate.nil at basis(2), 0 with *1334  have n1 := coordinate.nil at basis(2), 1 with *1335  have n2 := coordinate.nil at basis(2), 2 with *1336  have value0 : coordinate(1 :: [], basis(2), 0) = (0:R)1337    rw [c0, n0, e0]1338    ring1339  have value1 : coordinate(1 :: [], basis(2), 1) = (4:R)1340    rw [c1, n1, n2, e1, e2]1341    ring1342  have value2 : coordinate(1 :: [], basis(2), 2) = (3:R)1343    rw [c2, n1, n2, e1, e2]1344    ring1345  have three := IntReal.numeral at 31346  have four := IntReal.numeral at 41347  have zero := IntReal.zero1348  have one := IntReal.one1349  have negative := IntReal.sub with zero, one1350  have multiple := Div5.five with negative1351  have residue : Div5((3:R) - 2 * (4:R))1352    have same : (3:R) - 2 * (4:R) = 5 * ((0:R) - (1:R)) by ring1353    rw same1354    exact multiple1355  have relation := HeadRelation.one at (0:R), (4:R), (3:R) with Div5.zero, residue1356  unfold Swierczkowski1357  rw [value0, value1, value2]1358  exact ⟨zero, four, three, Div5.not_four, relation⟩13591360-- Along a reduced word ending in the letter x, the invariant from a start1361-- vector adapted to x holds with the word's first letter.1362theorem Swierczkowski.of_last (w : List(4)) (x v : Set)1363  requires letter : x ∈ 41364  requires vector : v : 3 → ℝ1365  requires base : Swierczkowski(x, [], v)1366  requires reduced : Reduced(w)1367  requires shape : ∃ u, List(4, u) ∧ w = append{A := 4}(x :: [], u)1368  shows ∃ ℓ ∈ 4, ∃ rest, List(4, rest) ∧ w = ℓ :: rest ∧ Swierczkowski(ℓ, rest, v)1369proof1370  induction w1371  | List.nil =>1372    intros reduced shape1373    obtain ⟨u, listU, equal⟩ := shape1374    symm at equal1375    have parts := append.nil_iff.forward with equal1376    have distinct := List.cons_ne_nil at 4, x, [] with letter1377    exfalso1378    exact distinct with parts.right1379  | List.cons(ℓ, rest) using ih =>1380    intros reduced shape1381    have letterL : ℓ ∈ 4 by assumption1382    have listRest : List(4, rest) by assumption1383    obtain ⟨u, listU, equal⟩ := shape1384    have cases := List.cases at 4, u with listU1385    cases cases with empty | consU1386    . have single : List(4, x :: []) by typecheck1387      have nilCase := append.nil at 4, x :: [] with single1388      rw [empty, nilCase] at equal1389      have both := List.cons_injective at 4, ℓ, x, rest, [] with letterL, letter, equal1390      obtain ⟨headEq, tailEq⟩ := both1391      refine ⟨ℓ, letterL, rest, listRest, rfl, ?_⟩1392      rw [headEq, tailEq]1393      exact base1394    . obtain ⟨y, letterY, tail, listTail, shapeU⟩ := consU1395      have single : List(4, x :: []) by typecheck1396      have consCase := append.cons at 4, y, tail, x :: [] with letterY1397      rw [shapeU, consCase] at equal1398      have both := List.cons_injective at 4, ℓ, y, rest, append{A := 4}(x :: [], tail)1399        with letterL, letterY, equal1400      obtain ⟨headEq, tailEq⟩ := both1401      have reducedRest := Reduced.tail at ℓ, rest with letterL, reduced1402      have shapeRest : ∃ u, List(4, u) ∧ rest = append{A := 4}(x :: [], u)1403        exact ⟨tail, listTail, tailEq⟩1404      obtain ⟨h, letterH, rest2, listRest2, shapeRest2, invariant⟩ := ih with reducedRest,1405        shapeRest1406      rw shapeRest2 at reduced1407      have criterion := Reduced.cons_cons.forward at ℓ, h, rest2 with letterL, letterH, reduced1408      have notInverse := cancels.false_iff.forward with criterion.left1409      have stepped := Swierczkowski.step with letterL, letterH, notInverse, vector, invariant1410      refine ⟨ℓ, letterL, h :: rest2, ?_, ?_, stepped⟩1411      . typecheck1412      . rw shapeRest21413        rfl14141415-- The freeness theorem: a nonempty reduced word is not the identity.1416theorem wordRotation.ne_one (w : List(4))1417  requires reduced : Reduced(w)1418  requires nonempty : w ≠ []1419  shows wordRotation(w) ≠ Ring.one(matrixRing(realRing, 3))1420proof1421  intro trivial1422  have shape := List.snoc_cases at 4, w with *1423  cases shape with empty | snoc1424  . exact nonempty with empty1425  . obtain ⟨x, letter, front, listFront, equal⟩ := snoc1426    have finish : ∀ v, (v : 3 → ℝ) → v(1) = (0:R) → Swierczkowski(x, [], v) → ⊥1427      intros v vector zero base1428      have shapeW : ∃ u, List(4, u) ∧ w = append{A := 4}(x :: [], u)1429        exact ⟨front, listFront, equal⟩1430      obtain ⟨ℓ, letterL, rest, listRest, split, invariant⟩ := Swierczkowski.of_last at w, x, v1431        with letter, vector, base, reduced, shapeW1432      obtain ⟨intA, intB, intC, nonzero, relation⟩ := invariant1433      have scale := fivePow.real at w1434      have value : coordinate(ℓ :: rest, v, 1) = (0:R)1435        rw [coordinate.value, ← split, trivial, matrixVector.one, zero]1436        ring1437      apply nonzero1438      rw value1439      exact Div5.zero1440    have alternatives := letter.cases with letter1441    rcases alternatives with at0 | at1 | at2 | at31442    . have vector := basis.vector at 2 with *1443      have zero := basis.other at 1, 2 with index.one_mem, index.two_mem, index.one_ne_two1444      have target := finish with basis(2), vector, zero1445      rw at0 at target1446      exact target with Swierczkowski.base_a1447    . have vector := basis.vector at 2 with *1448      have zero := basis.other at 1, 2 with index.one_mem, index.two_mem, index.one_ne_two1449      have target := finish with basis(2), vector, zero1450      rw at1 at target1451      exact target with Swierczkowski.base_at1452    . have vector := basis.vector at 0 with *1453      have zero := basis.other at 1, 0 with index.one_mem, index.zero_mem, index.one_ne_zero1454      have target := finish with basis(0), vector, zero1455      rw at2 at target1456      exact target with Swierczkowski.base_b1457    . have vector := basis.vector at 0 with *1458      have zero := basis.other at 1, 0 with index.one_mem, index.zero_mem, index.one_ne_zero1459      have target := finish with basis(0), vector, zero1460      rw at3 at target1461      exact target with Swierczkowski.base_bt14621463theorem wordRotation.ne_unit (w : List(4))1464  requires reduced : Reduced(w)1465  requires nonempty : w ≠ []1466  shows wordRotation(w) ≠ Group.one(SO3)1467proof1468  rw SO3.oneOf1469  exact wordRotation.ne_one with reduced, nonempty14701471-- The word ab is not the identity.1472theorem wordRotation.sample1473  shows wordRotation(0 :: 2 :: []) ≠ Ring.one(matrixRing(realRing, 3))1474proof1475  have reduced : Reduced(0 :: 2 :: [])1476    unfold Reduced1477    compute1478  have nonempty : 0 :: 2 :: [] ≠ []1479    have tail := List.closed_cons at 4, 2, [] with letterIn.two1480    exact List.cons_ne_nil at 4, 0, 2 :: [] with tail, letterIn.zero1481  have tail := List.closed_cons at 4, 2, [] with letterIn.two1482  have word := List.closed_cons at 4, 0, 2 :: [] with tail, letterIn.zero1483  exact wordRotation.ne_one with word, reduced, nonempty1484