-- The rotation of a word in the generators a, a⁻¹, b, b⁻¹ and the freeness
-- theorem: a nonempty reduced word is not the identity rotation, by
-- Swierczkowski's argument on integer vectors modulo 5
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Rotation.Freeness
import Generators
import Algebra.Group.Words
import Real.Integer

-- The matrix of a letter: 0, 1, 2, 3 read rotA, rotA⁻¹, rotB, rotB⁻¹.
def letterMatrix (ℓ : Nat) → Set
  | zero => rotA
  | succ(k) => pick3(transpose(rotA), rotB, transpose(rotB), k)

theorem letterMatrix.zero
  shows letterMatrix(0) = rotA
proof
  simp [letterMatrix]

theorem letterMatrix.one
  shows letterMatrix(1) = transpose(rotA)
proof
  simp [letterMatrix, pick3]

theorem letterMatrix.two
  shows letterMatrix(2) = rotB
proof
  simp [letterMatrix, pick3, pick2]

theorem letterMatrix.three
  shows letterMatrix(3) = transpose(rotB)
proof
  simp [letterMatrix, pick3, pick2]

theorem letterMatrix.so3 (ℓ : Set)
  requires letter : ℓ ∈ 4
  shows letterMatrix(ℓ) ∈ so3Matrices
proof
  have alternatives := letter.cases with letter
  rcases alternatives with at0 | at1 | at2 | at3
  . rw [at0, letterMatrix.zero]
    exact rotA.so3
  . rw [at1, letterMatrix.one]
    exact rotA.transpose_so3
  . rw [at2, letterMatrix.two]
    exact rotB.so3
  . rw [at3, letterMatrix.three]
    exact rotB.transpose_so3

instance letterMatrix.matrix (ℓ : Set)
  requires letter : ℓ ∈ 4
  shows letterMatrix(ℓ) : realRing ^ 3 × 3
proof
  exact so3Matrices.matrix with (letterMatrix.so3 with letter)

-- The rotation of a word: the product of the matrices of its letters.
def wordRotation (w : List(4)) → Set
  | [] => Ring.one(matrixRing(realRing, 3))
  | ℓ :: rest => call2(Ring.mul(matrixRing(realRing, 3)), letterMatrix(ℓ), wordRotation(rest))

theorem wordRotation.nil
  shows wordRotation([]) = Ring.one(matrixRing(realRing, 3))
proof
  simp [wordRotation]

theorem wordRotation.cons (ℓ : Set) (rest : List(4))
  requires letter : ℓ ∈ 4
  shows wordRotation(ℓ :: rest) =
    Ring.mul(matrixRing(realRing, 3))(letterMatrix(ℓ), wordRotation(rest))
proof
  simp [wordRotation]

theorem wordRotation.so3 (w : List(4))
  shows wordRotation(w) ∈ so3Matrices
proof
  induction w
  | List.nil =>
    rw wordRotation.nil
    exact so3Matrices.one_mem
  | List.cons(ℓ, rest) using ih =>
    have letter : ℓ ∈ 4 by assumption
    have head := letterMatrix.so3 with letter
    have headMatrix := so3Matrices.matrix with head
    have restMatrix := so3Matrices.matrix with ih
    rw wordRotation.cons
    exact so3Matrices.mul_mem with head, ih

instance wordRotation.matrix (w : List(4))
  shows wordRotation(w) : realRing ^ 3 × 3
proof
  have member := wordRotation.so3 at w with *
  exact so3Matrices.matrix with member

-- The scale 5^k of a word of length k, as a recursion on the word.
def fivePow (w : List(4)) → Set
  | [] => (1:R)
  | ℓ :: rest => (5:R) * (fivePow(rest):R)

theorem fivePow.nil
  shows fivePow([]) = (1:R)
proof
  simp [fivePow]

theorem fivePow.cons (ℓ : Set) (rest : List(4))
  requires letter : ℓ ∈ 4
  shows fivePow(ℓ :: rest) = (5:R) * (fivePow(rest):R)
proof
  simp [fivePow]

instance fivePow.real (w : List(4))
  shows fivePow(w) ∈ ℝ
proof
  induction w
  | List.nil =>
    rw fivePow.nil
    typecheck
  | List.cons(ℓ, rest) using ih =>
    have letter : ℓ ∈ 4 by assumption
    rw fivePow.cons
    typecheck

-- The scaled coordinates of the path of a word from a start vector v:
-- 5^k times the i-th coordinate of wordRotation(w) · v.
def coordinate (w v i : Set) : Set :=
  (fivePow(w):R) * ((wordRotation(w) · v)(i):R)

theorem coordinate.value (w v i : Set)
  shows coordinate(w, v, i) = (fivePow(w):R) * ((wordRotation(w) · v)(i):R)
proof
  simp [coordinate]

-- Five times the action of each generator, in integer form.
theorem rotA.five_action (u : Set)
  requires vector : u : 3 → ℝ
  shows (5:R) * ((rotA · u)(0):R) = 5 * (u(0):R) ∧
    (5:R) * ((rotA · u)(1):R) = 3 * (u(1):R) - 4 * (u(2):R) ∧
    (5:R) * ((rotA · u)(2):R) = 4 * (u(1):R) + 3 * (u(2):R)
proof
  obtain ⟨a00, a01, a02, a10, a11, a12, a20, a21, a22⟩ := rotA.entries
  have five := fifth.five
  have u0 := vector.component_real at u, 0 with *
  have u1 := vector.component_real at u, 1 with *
  have u2 := vector.component_real at u, 2 with *
  have e0 := matrixVector.entry at rotA, u, 0 with *
  have e1 := matrixVector.entry at rotA, u, 1 with *
  have e2 := matrixVector.entry at rotA, u, 2 with *
  rw [e0, e1, e2, a00, a01, a02, a10, a11, a12, a20, a21, a22]
  have scale1 : fifth * 5 * (3 * (u(1):R) - 4 * (u(2):R)) = 3 * (u(1):R) - 4 * (u(2):R)
    rw five
    ring
  have scale2 : fifth * 5 * (4 * (u(1):R) + 3 * (u(2):R)) = 4 * (u(1):R) + 3 * (u(2):R)
    rw five
    ring
  constructor
  . ring
  . constructor
    . calc
        (5:R) * ((0:R) * (u(0):R) + 3 * fifth * (u(1):R) + -(4 * fifth) * (u(2):R)) =
            fifth * 5 * (3 * (u(1):R) - 4 * (u(2):R)) := by ring
        _ = 3 * (u(1):R) - 4 * (u(2):R) := scale1
    . calc
        (5:R) * ((0:R) * (u(0):R) + 4 * fifth * (u(1):R) + 3 * fifth * (u(2):R)) =
            fifth * 5 * (4 * (u(1):R) + 3 * (u(2):R)) := by ring
        _ = 4 * (u(1):R) + 3 * (u(2):R) := scale2

theorem rotA.transpose_five_action (u : Set)
  requires vector : u : 3 → ℝ
  shows (5:R) * ((transpose(rotA) · u)(0):R) = 5 * (u(0):R) ∧
    (5:R) * ((transpose(rotA) · u)(1):R) = 3 * (u(1):R) + 4 * (u(2):R) ∧
    (5:R) * ((transpose(rotA) · u)(2):R) = 3 * (u(2):R) - 4 * (u(1):R)
proof
  obtain ⟨a00, a01, a02, a10, a11, a12, a20, a21, a22⟩ := rotA.entries
  have five := fifth.five
  have transposed := transpose.matrix at rotA with *
  have u0 := vector.component_real at u, 0 with *
  have u1 := vector.component_real at u, 1 with *
  have u2 := vector.component_real at u, 2 with *
  have e0 := matrixVector.entry at transpose(rotA), u, 0 with *
  have e1 := matrixVector.entry at transpose(rotA), u, 1 with *
  have e2 := matrixVector.entry at transpose(rotA), u, 2 with *
  have t00 := transpose.entry at rotA, 0, 0 with *
  have t01 := transpose.entry at rotA, 0, 1 with *
  have t02 := transpose.entry at rotA, 0, 2 with *
  have t10 := transpose.entry at rotA, 1, 0 with *
  have t11 := transpose.entry at rotA, 1, 1 with *
  have t12 := transpose.entry at rotA, 1, 2 with *
  have t20 := transpose.entry at rotA, 2, 0 with *
  have t21 := transpose.entry at rotA, 2, 1 with *
  have t22 := transpose.entry at rotA, 2, 2 with *
  rw [e0, e1, e2, t00, t01, t02, t10, t11, t12, t20, t21, t22,
    a00, a01, a02, a10, a11, a12, a20, a21, a22]
  have scale1 : fifth * 5 * (3 * (u(1):R) + 4 * (u(2):R)) = 3 * (u(1):R) + 4 * (u(2):R)
    rw five
    ring
  have scale2 : fifth * 5 * (3 * (u(2):R) - 4 * (u(1):R)) = 3 * (u(2):R) - 4 * (u(1):R)
    rw five
    ring
  constructor
  . ring
  . constructor
    . calc
        (5:R) * ((0:R) * (u(0):R) + 3 * fifth * (u(1):R) + 4 * fifth * (u(2):R)) =
            fifth * 5 * (3 * (u(1):R) + 4 * (u(2):R)) := by ring
        _ = 3 * (u(1):R) + 4 * (u(2):R) := scale1
    . calc
        (5:R) * ((0:R) * (u(0):R) + -(4 * fifth) * (u(1):R) + 3 * fifth * (u(2):R)) =
            fifth * 5 * (3 * (u(2):R) - 4 * (u(1):R)) := by ring
        _ = 3 * (u(2):R) - 4 * (u(1):R) := scale2

theorem rotB.five_action (u : Set)
  requires vector : u : 3 → ℝ
  shows (5:R) * ((rotB · u)(0):R) = 3 * (u(0):R) - 4 * (u(1):R) ∧
    (5:R) * ((rotB · u)(1):R) = 4 * (u(0):R) + 3 * (u(1):R) ∧
    (5:R) * ((rotB · u)(2):R) = 5 * (u(2):R)
proof
  obtain ⟨b00, b01, b02, b10, b11, b12, b20, b21, b22⟩ := rotB.entries
  have five := fifth.five
  have u0 := vector.component_real at u, 0 with *
  have u1 := vector.component_real at u, 1 with *
  have u2 := vector.component_real at u, 2 with *
  have e0 := matrixVector.entry at rotB, u, 0 with *
  have e1 := matrixVector.entry at rotB, u, 1 with *
  have e2 := matrixVector.entry at rotB, u, 2 with *
  rw [e0, e1, e2, b00, b01, b02, b10, b11, b12, b20, b21, b22]
  have scale0 : fifth * 5 * (3 * (u(0):R) - 4 * (u(1):R)) = 3 * (u(0):R) - 4 * (u(1):R)
    rw five
    ring
  have scale1 : fifth * 5 * (4 * (u(0):R) + 3 * (u(1):R)) = 4 * (u(0):R) + 3 * (u(1):R)
    rw five
    ring
  constructor
  . calc
      (5:R) * (3 * fifth * (u(0):R) + -(4 * fifth) * (u(1):R) + (0:R) * (u(2):R)) =
          fifth * 5 * (3 * (u(0):R) - 4 * (u(1):R)) := by ring
      _ = 3 * (u(0):R) - 4 * (u(1):R) := scale0
  . constructor
    . calc
        (5:R) * (4 * fifth * (u(0):R) + 3 * fifth * (u(1):R) + (0:R) * (u(2):R)) =
            fifth * 5 * (4 * (u(0):R) + 3 * (u(1):R)) := by ring
        _ = 4 * (u(0):R) + 3 * (u(1):R) := scale1
    . ring

theorem rotB.transpose_five_action (u : Set)
  requires vector : u : 3 → ℝ
  shows (5:R) * ((transpose(rotB) · u)(0):R) = 3 * (u(0):R) + 4 * (u(1):R) ∧
    (5:R) * ((transpose(rotB) · u)(1):R) = 3 * (u(1):R) - 4 * (u(0):R) ∧
    (5:R) * ((transpose(rotB) · u)(2):R) = 5 * (u(2):R)
proof
  obtain ⟨b00, b01, b02, b10, b11, b12, b20, b21, b22⟩ := rotB.entries
  have five := fifth.five
  have transposed := transpose.matrix at rotB with *
  have u0 := vector.component_real at u, 0 with *
  have u1 := vector.component_real at u, 1 with *
  have u2 := vector.component_real at u, 2 with *
  have e0 := matrixVector.entry at transpose(rotB), u, 0 with *
  have e1 := matrixVector.entry at transpose(rotB), u, 1 with *
  have e2 := matrixVector.entry at transpose(rotB), u, 2 with *
  have t00 := transpose.entry at rotB, 0, 0 with *
  have t01 := transpose.entry at rotB, 0, 1 with *
  have t02 := transpose.entry at rotB, 0, 2 with *
  have t10 := transpose.entry at rotB, 1, 0 with *
  have t11 := transpose.entry at rotB, 1, 1 with *
  have t12 := transpose.entry at rotB, 1, 2 with *
  have t20 := transpose.entry at rotB, 2, 0 with *
  have t21 := transpose.entry at rotB, 2, 1 with *
  have t22 := transpose.entry at rotB, 2, 2 with *
  rw [e0, e1, e2, t00, t01, t02, t10, t11, t12, t20, t21, t22,
    b00, b01, b02, b10, b11, b12, b20, b21, b22]
  have scale0 : fifth * 5 * (3 * (u(0):R) + 4 * (u(1):R)) = 3 * (u(0):R) + 4 * (u(1):R)
    rw five
    ring
  have scale1 : fifth * 5 * (3 * (u(1):R) - 4 * (u(0):R)) = 3 * (u(1):R) - 4 * (u(0):R)
    rw five
    ring
  constructor
  . calc
      (5:R) * (3 * fifth * (u(0):R) + 4 * fifth * (u(1):R) + (0:R) * (u(2):R)) =
          fifth * 5 * (3 * (u(0):R) + 4 * (u(1):R)) := by ring
      _ = 3 * (u(0):R) + 4 * (u(1):R) := scale0
  . constructor
    . calc
        (5:R) * (-(4 * fifth) * (u(0):R) + 3 * fifth * (u(1):R) + (0:R) * (u(2):R)) =
            fifth * 5 * (3 * (u(1):R) - 4 * (u(0):R)) := by ring
        _ = 3 * (u(1):R) - 4 * (u(0):R) := scale1
    . ring

-- Integer-valued reals, as differences of naturals, and the multiples of
-- five among them.
predicate IntReal (x : Set) :=
  ∃ m ∈ ℕ, ∃ n ∈ ℕ, x = (realNat(m):R) - (realNat(n):R)
predicate Div5 (x : Set) :=
  ∃ m ∈ ℕ, ∃ n ∈ ℕ, x = 5 * (realNat(m):R) - 5 * (realNat(n):R)

theorem IntReal.real (x : Set)
  requires integral : IntReal(x)
  shows x ∈ ℝ
proof
  obtain ⟨m, hm, n, hn, equal⟩ := integral
  have natM := nat.omega.backward with hm
  have natN := nat.omega.backward with hn
  rw equal
  typecheck

-- The integer-valued reals are exactly the image of ℤ under realInt.
theorem IntReal.iff_realInt (x : Set)
  shows IntReal(x) ↔ ∃ z ∈ ℤ, x = realInt(z)
proof
  have range := realInt.range at x
  unfold IntReal
  constructor
  . intro difference
    exact range.backward with difference
  . intro image
    exact range.forward with image

theorem IntReal.nat (k : Nat)
  shows IntReal(realNat(k))
proof
  have kIn : k ∈ ℕ := nat.omega.forward with assumption
  have zeroIn : 0 ∈ ℕ := nat.omega.forward at 0 with *
  unfold IntReal
  refine ⟨k, kIn, 0, zeroIn, ?_⟩
  rw realNat.zero
  ring

theorem IntReal.numeral (k : Nat)
  shows IntReal(realNumeral(k))
proof
  unfold realNumeral
  exact IntReal.nat at k

theorem IntReal.zero
  shows IntReal((0:R))
proof
  have natural := IntReal.nat at 0
  rw realNat.zero at natural
  exact natural

theorem IntReal.one
  shows IntReal((1:R))
proof
  have natural := IntReal.nat at 1
  rw realNat.one at natural
  exact natural

theorem IntReal.add (x y : Set)
  requires integralX : IntReal(x)
  requires integralY : IntReal(y)
  shows IntReal((x:R) + (y:R))
proof
  obtain ⟨m, hm, n, hn, equalX⟩ := integralX
  obtain ⟨p, hp, q, hq, equalY⟩ := integralY
  have natM := nat.omega.backward with hm
  have natN := nat.omega.backward with hn
  have natP := nat.omega.backward with hp
  have natQ := nat.omega.backward with hq
  have sumIn : add(m, p) ∈ ℕ := nat.omega.forward at add(m, p) with *
  have sumIn2 : add(n, q) ∈ ℕ := nat.omega.forward at add(n, q) with *
  unfold IntReal
  refine ⟨add(m, p), sumIn, add(n, q), sumIn2, ?_⟩
  rw [equalX, equalY, realNat.add, realNat.add]
  ring

theorem IntReal.neg (x : Set)
  requires integral : IntReal(x)
  shows IntReal(-(x:R))
proof
  obtain ⟨m, hm, n, hn, equal⟩ := integral
  have natM := nat.omega.backward with hm
  have natN := nat.omega.backward with hn
  unfold IntReal
  refine ⟨n, hn, m, hm, ?_⟩
  rw equal
  ring

theorem IntReal.sub (x y : Set)
  requires integralX : IntReal(x)
  requires integralY : IntReal(y)
  shows IntReal((x:R) - (y:R))
proof
  have realX := IntReal.real with integralX
  have realY := IntReal.real with integralY
  have negative := IntReal.neg with integralY
  have sum := IntReal.add with integralX, negative
  have same : (x:R) - (y:R) = (x:R) + -(y:R) by ring
  rw same
  exact sum

theorem IntReal.mul (x y : Set)
  requires integralX : IntReal(x)
  requires integralY : IntReal(y)
  shows IntReal((x:R) * (y:R))
proof
  obtain ⟨m, hm, n, hn, equalX⟩ := integralX
  obtain ⟨p, hp, q, hq, equalY⟩ := integralY
  have natM := nat.omega.backward with hm
  have natN := nat.omega.backward with hn
  have natP := nat.omega.backward with hp
  have natQ := nat.omega.backward with hq
  have firstIn : add(mul(m, p), mul(n, q)) ∈ ℕ := nat.omega.forward at add(mul(m, p), mul(n, q)) with *
  have secondIn : add(mul(m, q), mul(n, p)) ∈ ℕ := nat.omega.forward at add(mul(m, q), mul(n, p)) with *
  unfold IntReal
  refine ⟨add(mul(m, p), mul(n, q)), firstIn, add(mul(m, q), mul(n, p)), secondIn, ?_⟩
  rw [equalX, equalY, realNat.add, realNat.add, realNat.mul, realNat.mul,
    realNat.mul, realNat.mul]
  ring

theorem Div5.real (x : Set)
  requires divisible : Div5(x)
  shows x ∈ ℝ
proof
  obtain ⟨m, hm, n, hn, equal⟩ := divisible
  have natM := nat.omega.backward with hm
  have natN := nat.omega.backward with hn
  rw equal
  typecheck

theorem Div5.zero
  shows Div5((0:R))
proof
  have zeroIn : 0 ∈ ℕ := nat.omega.forward at 0 with *
  unfold Div5
  refine ⟨0, zeroIn, 0, zeroIn, ?_⟩
  rw realNat.zero
  ring

theorem Div5.of_eq (x y : Set)
  requires divisible : Div5(x)
  requires equal : y = x
  shows Div5(y)
proof
  rw equal
  exact divisible

theorem Div5.add (x y : Set)
  requires divisibleX : Div5(x)
  requires divisibleY : Div5(y)
  shows Div5((x:R) + (y:R))
proof
  obtain ⟨m, hm, n, hn, equalX⟩ := divisibleX
  obtain ⟨p, hp, q, hq, equalY⟩ := divisibleY
  have natM := nat.omega.backward with hm
  have natN := nat.omega.backward with hn
  have natP := nat.omega.backward with hp
  have natQ := nat.omega.backward with hq
  have sumIn : add(m, p) ∈ ℕ := nat.omega.forward at add(m, p) with *
  have sumIn2 : add(n, q) ∈ ℕ := nat.omega.forward at add(n, q) with *
  unfold Div5
  refine ⟨add(m, p), sumIn, add(n, q), sumIn2, ?_⟩
  rw [equalX, equalY, realNat.add, realNat.add]
  ring

theorem Div5.neg (x : Set)
  requires divisible : Div5(x)
  shows Div5(-(x:R))
proof
  obtain ⟨m, hm, n, hn, equal⟩ := divisible
  have natM := nat.omega.backward with hm
  have natN := nat.omega.backward with hn
  unfold Div5
  refine ⟨n, hn, m, hm, ?_⟩
  rw equal
  ring

theorem Div5.sub (x y : Set)
  requires divisibleX : Div5(x)
  requires divisibleY : Div5(y)
  shows Div5((x:R) - (y:R))
proof
  have realX := Div5.real with divisibleX
  have realY := Div5.real with divisibleY
  have negative := Div5.neg with divisibleY
  have sum := Div5.add with divisibleX, negative
  have same : (x:R) - (y:R) = (x:R) + -(y:R) by ring
  rw same
  exact sum

theorem Div5.mul_int (x y : Set)
  requires divisible : Div5(x)
  requires integral : IntReal(y)
  shows Div5((x:R) * (y:R))
proof
  obtain ⟨m, hm, n, hn, equalX⟩ := divisible
  obtain ⟨p, hp, q, hq, equalY⟩ := integral
  have natM := nat.omega.backward with hm
  have natN := nat.omega.backward with hn
  have natP := nat.omega.backward with hp
  have natQ := nat.omega.backward with hq
  have firstIn : add(mul(m, p), mul(n, q)) ∈ ℕ := nat.omega.forward at add(mul(m, p), mul(n, q)) with *
  have secondIn : add(mul(m, q), mul(n, p)) ∈ ℕ := nat.omega.forward at add(mul(m, q), mul(n, p)) with *
  unfold Div5
  refine ⟨add(mul(m, p), mul(n, q)), firstIn, add(mul(m, q), mul(n, p)), secondIn, ?_⟩
  rw [equalX, equalY, realNat.add, realNat.add, realNat.mul, realNat.mul,
    realNat.mul, realNat.mul]
  ring

theorem Div5.five (x : Set)
  requires integral : IntReal(x)
  shows Div5(5 * (x:R))
proof
  obtain ⟨m, hm, n, hn, equal⟩ := integral
  have natM := nat.omega.backward with hm
  have natN := nat.omega.backward with hn
  unfold Div5
  refine ⟨m, hm, n, hn, ?_⟩
  rw equal
  ring

-- A multiple of five that is three times an integer: the integer itself
-- is a multiple of five.
theorem Div5.of_three (x : Set)
  requires integral : IntReal(x)
  requires divisible : Div5(3 * (x:R))
  shows Div5(x)
proof
  have realX := IntReal.real with integral
  have two := IntReal.numeral at 2
  have doubled := Div5.mul_int with divisible, two
  have fived := Div5.five with integral
  have difference := Div5.sub with doubled, fived
  have same : (x:R) = 3 * (x:R) * 2 - 5 * (x:R) by ring
  exact Div5.of_eq with difference, same

-- Neither 4 nor −4 is a multiple of five.
theorem Div5.not_four
  shows ¬Div5((4:R))
proof
  intro divisible
  obtain ⟨m, hm, n, hn, equal⟩ := divisible
  have natM := nat.omega.backward with hm
  have natN := nat.omega.backward with hn
  have cast : (realNat(add(4, mul(5, n))):R) = realNat(mul(5, m))
    have fourCast : (realNat(4):R) = (4:R)
      unfold realNumeral
      rfl
    have fiveCast : (realNat(5):R) = (5:R)
      unfold realNumeral
      rfl
    rw [realNat.add, realNat.mul, realNat.mul, fourCast, fiveCast]
    linarith
  have natural := realNat.injective with cast
  have cases := Less.trichotomy at m, n with natM, natN
  rcases cases with less | same | greater
  . arith
  . arith
  . arith

theorem Div5.not_neg_four
  shows ¬Div5((0:R) - 4)
proof
  intro divisible
  obtain ⟨m, hm, n, hn, equal⟩ := divisible
  have natM := nat.omega.backward with hm
  have natN := nat.omega.backward with hn
  have cast : (realNat(add(4, mul(5, m))):R) = realNat(mul(5, n))
    have fourCast : (realNat(4):R) = (4:R)
      unfold realNumeral
      rfl
    have fiveCast : (realNat(5):R) = (5:R)
      unfold realNumeral
      rfl
    rw [realNat.add, realNat.mul, realNat.mul, fourCast, fiveCast]
    linarith
  have natural := realNat.injective with cast
  have cases := Less.trichotomy at m, n with natM, natN
  rcases cases with less | same | greater
  . arith
  . arith
  . arith

-- The letter 3 differs from the others.
theorem letter.zero_ne_three
  shows 0 ≠ 3
proof
  intro equal
  arith

theorem letter.one_ne_three
  shows 1 ≠ 3
proof
  intro equal
  arith

theorem letter.two_ne_three
  shows 2 ≠ 3
proof
  intro equal
  arith

theorem letter.three_ne_zero
  shows 3 ≠ 0
proof
  intro equal
  arith

theorem letter.three_ne_one
  shows 3 ≠ 1
proof
  intro equal
  arith

theorem letter.three_ne_two
  shows 3 ≠ 2
proof
  intro equal
  arith

-- The residues modulo 5 forced on the integer vector (a, b, c) by the
-- first letter h of the word: after a rotation about the x-axis the first
-- coordinate is a multiple of five and the third is 3b or 2b modulo 5;
-- after one about the z-axis the third coordinate is a multiple of five
-- and the second is 3a or 2a modulo 5.
predicate HeadRelation (h a b c : Set) :=
  (h = 0 → Div5(a) ∧ Div5((c:R) - 3 * (b:R))) ∧
  (h = 1 → Div5(a) ∧ Div5((c:R) - 2 * (b:R))) ∧
  (h = 2 → Div5(c) ∧ Div5((b:R) - 3 * (a:R))) ∧
  (h = 3 → Div5(c) ∧ Div5((b:R) - 2 * (a:R)))

theorem HeadRelation.zero (a b c : Set)
  requires first : Div5(a)
  requires third : Div5((c:R) - 3 * (b:R))
  shows HeadRelation(0, a, b, c)
proof
  unfold HeadRelation
  constructor
  . intro equal
    exact ⟨first, third⟩
  . constructor
    . intro equal
      exfalso
      exact index.zero_ne_one with equal
    . constructor
      . intro equal
        exfalso
        exact index.zero_ne_two with equal
      . intro equal
        exfalso
        exact letter.zero_ne_three with equal

theorem HeadRelation.one (a b c : Set)
  requires first : Div5(a)
  requires third : Div5((c:R) - 2 * (b:R))
  shows HeadRelation(1, a, b, c)
proof
  unfold HeadRelation
  constructor
  . intro equal
    exfalso
    exact index.one_ne_zero with equal
  . constructor
    . intro equal
      exact ⟨first, third⟩
    . constructor
      . intro equal
        exfalso
        exact index.one_ne_two with equal
      . intro equal
        exfalso
        exact letter.one_ne_three with equal

theorem HeadRelation.two (a b c : Set)
  requires third : Div5(c)
  requires second : Div5((b:R) - 3 * (a:R))
  shows HeadRelation(2, a, b, c)
proof
  unfold HeadRelation
  constructor
  . intro equal
    exfalso
    exact index.two_ne_zero with equal
  . constructor
    . intro equal
      exfalso
      exact index.two_ne_one with equal
    . constructor
      . intro equal
        exact ⟨third, second⟩
      . intro equal
        exfalso
        exact letter.two_ne_three with equal

theorem HeadRelation.three (a b c : Set)
  requires third : Div5(c)
  requires second : Div5((b:R) - 2 * (a:R))
  shows HeadRelation(3, a, b, c)
proof
  unfold HeadRelation
  constructor
  . intro equal
    exfalso
    exact letter.three_ne_zero with equal
  . constructor
    . intro equal
      exfalso
      exact letter.three_ne_one with equal
    . constructor
      . intro equal
        exfalso
        exact letter.three_ne_two with equal
      . intro equal
        exact ⟨third, second⟩

-- One step of Swierczkowski's argument for each generator: from an
-- integer vector (a, b, c) with b not a multiple of five, whose residues
-- are those of a word with first letter h, the vector after the letter
-- ℓ ≠ h⁻¹ again has a middle coordinate that is not a multiple of five.
theorem step.rotA (a b c h : Set)
  requires intA : IntReal(a)
  requires intB : IntReal(b)
  requires intC : IntReal(c)
  requires nonzero : ¬Div5(b)
  requires relation : HeadRelation(h, a, b, c)
  requires letter : h ∈ 4
  requires reduced : h ≠ 1
  shows IntReal(5 * (a:R)) ∧ IntReal(3 * (b:R) - 4 * (c:R)) ∧
    IntReal(4 * (b:R) + 3 * (c:R)) ∧ ¬Div5(3 * (b:R) - 4 * (c:R)) ∧
    HeadRelation(0, 5 * (a:R), 3 * (b:R) - 4 * (c:R), 4 * (b:R) + 3 * (c:R))
proof
  have realA := IntReal.real with intA
  have realB := IntReal.real with intB
  have realC := IntReal.real with intC
  have two := IntReal.numeral at 2
  have three := IntReal.numeral at 3
  have four := IntReal.numeral at 4
  have five := IntReal.numeral at 5
  have eight := IntReal.numeral at 8
  have int5a := IntReal.mul with five, intA
  have int3b := IntReal.mul with three, intB
  have int4c := IntReal.mul with four, intC
  have int4b := IntReal.mul with four, intB
  have int3c := IntReal.mul with three, intC
  have int2b := IntReal.mul with two, intB
  have newB := IntReal.sub with int3b, int4c
  have newC := IntReal.add with int4b, int3c
  have newRelation : HeadRelation(0, 5 * (a:R), 3 * (b:R) - 4 * (c:R), 4 * (b:R) + 3 * (c:R))
    have divA := Div5.five with intA
    have combo := IntReal.sub with int3c, intB
    have divCombo := Div5.five with combo
    have same : (4 * (b:R) + 3 * (c:R)) - 3 * (3 * (b:R) - 4 * (c:R)) = 5 * (3 * (c:R) - (b:R)) by ring
    have divC := Div5.of_eq with divCombo, same
    exact HeadRelation.zero with divA, divC
  have newNonzero : ¬Div5(3 * (b:R) - 4 * (c:R))
    intro divisible
    obtain ⟨rel0, rel1, rel2, rel3⟩ := relation
    have alternatives := letter.cases with letter
    rcases alternatives with at0 | at1 | at2 | at3
    . obtain ⟨divA, divCB⟩ := rel0 with at0
      have t1 := Div5.mul_int with divCB, four
      have t2 := Div5.five with int2b
      have partial := Div5.add with divisible, t1
      have sum := Div5.add with partial, t2
      have same : (b:R) = (3 * (b:R) - 4 * (c:R)) + ((c:R) - 3 * (b:R)) * 4 + 5 * (2 * (b:R)) by ring
      exact nonzero with (Div5.of_eq with sum, same)
    . exact reduced with at1
    . obtain ⟨divC, divBA⟩ := rel2 with at2
      have t1 := Div5.mul_int with divisible, two
      have t2 := Div5.mul_int with divC, eight
      have t3 := Div5.five with intB
      have partial := Div5.add with t1, t2
      have combo := Div5.sub with partial, t3
      have same : (b:R) = (3 * (b:R) - 4 * (c:R)) * 2 + (c:R) * 8 - 5 * (b:R) by ring
      exact nonzero with (Div5.of_eq with combo, same)
    . obtain ⟨divC, divBA⟩ := rel3 with at3
      have t1 := Div5.mul_int with divisible, two
      have t2 := Div5.mul_int with divC, eight
      have t3 := Div5.five with intB
      have partial := Div5.add with t1, t2
      have combo := Div5.sub with partial, t3
      have same : (b:R) = (3 * (b:R) - 4 * (c:R)) * 2 + (c:R) * 8 - 5 * (b:R) by ring
      exact nonzero with (Div5.of_eq with combo, same)
  exact ⟨int5a, newB, newC, newNonzero, newRelation⟩

theorem step.rotA_transpose (a b c h : Set)
  requires intA : IntReal(a)
  requires intB : IntReal(b)
  requires intC : IntReal(c)
  requires nonzero : ¬Div5(b)
  requires relation : HeadRelation(h, a, b, c)
  requires letter : h ∈ 4
  requires reduced : h ≠ 0
  shows IntReal(5 * (a:R)) ∧ IntReal(3 * (b:R) + 4 * (c:R)) ∧
    IntReal(3 * (c:R) - 4 * (b:R)) ∧ ¬Div5(3 * (b:R) + 4 * (c:R)) ∧
    HeadRelation(1, 5 * (a:R), 3 * (b:R) + 4 * (c:R), 3 * (c:R) - 4 * (b:R))
proof
  have realA := IntReal.real with intA
  have realB := IntReal.real with intB
  have realC := IntReal.real with intC
  have two := IntReal.numeral at 2
  have three := IntReal.numeral at 3
  have four := IntReal.numeral at 4
  have five := IntReal.numeral at 5
  have eight := IntReal.numeral at 8
  have int5a := IntReal.mul with five, intA
  have int3b := IntReal.mul with three, intB
  have int4c := IntReal.mul with four, intC
  have int4b := IntReal.mul with four, intB
  have int3c := IntReal.mul with three, intC
  have int2b := IntReal.mul with two, intB
  have newB := IntReal.add with int3b, int4c
  have newC := IntReal.sub with int3c, int4b
  have newRelation : HeadRelation(1, 5 * (a:R), 3 * (b:R) + 4 * (c:R), 3 * (c:R) - 4 * (b:R))
    have divA := Div5.five with intA
    have negative := IntReal.neg with int2b
    have combo := IntReal.sub with negative, intC
    have divCombo := Div5.five with combo
    have same : (3 * (c:R) - 4 * (b:R)) - 2 * (3 * (b:R) + 4 * (c:R)) = 5 * (-(2 * (b:R)) - (c:R)) by ring
    have divC := Div5.of_eq with divCombo, same
    exact HeadRelation.one with divA, divC
  have newNonzero : ¬Div5(3 * (b:R) + 4 * (c:R))
    intro divisible
    obtain ⟨rel0, rel1, rel2, rel3⟩ := relation
    have alternatives := letter.cases with letter
    rcases alternatives with at0 | at1 | at2 | at3
    . exact reduced with at0
    . obtain ⟨divA, divCB⟩ := rel1 with at1
      have t1 := Div5.mul_int with divCB, four
      have t2 := Div5.five with int2b
      have partial := Div5.sub with divisible, t1
      have difference := Div5.sub with partial, t2
      have same : (b:R) = (3 * (b:R) + 4 * (c:R)) - ((c:R) - 2 * (b:R)) * 4 - 5 * (2 * (b:R)) by ring
      exact nonzero with (Div5.of_eq with difference, same)
    . obtain ⟨divC, divBA⟩ := rel2 with at2
      have t1 := Div5.mul_int with divisible, two
      have t2 := Div5.mul_int with divC, eight
      have t3 := Div5.five with intB
      have partial := Div5.sub with t1, t2
      have combo := Div5.sub with partial, t3
      have same : (b:R) = (3 * (b:R) + 4 * (c:R)) * 2 - (c:R) * 8 - 5 * (b:R) by ring
      exact nonzero with (Div5.of_eq with combo, same)
    . obtain ⟨divC, divBA⟩ := rel3 with at3
      have t1 := Div5.mul_int with divisible, two
      have t2 := Div5.mul_int with divC, eight
      have t3 := Div5.five with intB
      have partial := Div5.sub with t1, t2
      have combo := Div5.sub with partial, t3
      have same : (b:R) = (3 * (b:R) + 4 * (c:R)) * 2 - (c:R) * 8 - 5 * (b:R) by ring
      exact nonzero with (Div5.of_eq with combo, same)
  exact ⟨int5a, newB, newC, newNonzero, newRelation⟩

theorem step.rotB (a b c h : Set)
  requires intA : IntReal(a)
  requires intB : IntReal(b)
  requires intC : IntReal(c)
  requires nonzero : ¬Div5(b)
  requires relation : HeadRelation(h, a, b, c)
  requires letter : h ∈ 4
  requires reduced : h ≠ 3
  shows IntReal(3 * (a:R) - 4 * (b:R)) ∧ IntReal(4 * (a:R) + 3 * (b:R)) ∧
    IntReal(5 * (c:R)) ∧ ¬Div5(4 * (a:R) + 3 * (b:R)) ∧
    HeadRelation(2, 3 * (a:R) - 4 * (b:R), 4 * (a:R) + 3 * (b:R), 5 * (c:R))
proof
  have realA := IntReal.real with intA
  have realB := IntReal.real with intB
  have realC := IntReal.real with intC
  have two := IntReal.numeral at 2
  have three := IntReal.numeral at 3
  have four := IntReal.numeral at 4
  have five := IntReal.numeral at 5
  have int5c := IntReal.mul with five, intC
  have int3a := IntReal.mul with three, intA
  have int4b := IntReal.mul with four, intB
  have int4a := IntReal.mul with four, intA
  have int3b := IntReal.mul with three, intB
  have int2b := IntReal.mul with two, intB
  have newA := IntReal.sub with int3a, int4b
  have newB := IntReal.add with int4a, int3b
  have newRelation : HeadRelation(2, 3 * (a:R) - 4 * (b:R), 4 * (a:R) + 3 * (b:R), 5 * (c:R))
    have divC := Div5.five with intC
    have combo := IntReal.sub with int3b, intA
    have divCombo := Div5.five with combo
    have same : (4 * (a:R) + 3 * (b:R)) - 3 * (3 * (a:R) - 4 * (b:R)) = 5 * (3 * (b:R) - (a:R)) by ring
    have divB := Div5.of_eq with divCombo, same
    exact HeadRelation.two with divC, divB
  have newNonzero : ¬Div5(4 * (a:R) + 3 * (b:R))
    intro divisible
    obtain ⟨rel0, rel1, rel2, rel3⟩ := relation
    have alternatives := letter.cases with letter
    rcases alternatives with at0 | at1 | at2 | at3
    . obtain ⟨divA, divCB⟩ := rel0 with at0
      have t1 := Div5.mul_int with divA, four
      have difference := Div5.sub with divisible, t1
      have same : 3 * (b:R) = (4 * (a:R) + 3 * (b:R)) - (a:R) * 4 by ring
      have triple := Div5.of_eq with difference, same
      exact nonzero with (Div5.of_three with intB, triple)
    . obtain ⟨divA, divCB⟩ := rel1 with at1
      have t1 := Div5.mul_int with divA, four
      have difference := Div5.sub with divisible, t1
      have same : 3 * (b:R) = (4 * (a:R) + 3 * (b:R)) - (a:R) * 4 by ring
      have triple := Div5.of_eq with difference, same
      exact nonzero with (Div5.of_three with intB, triple)
    . obtain ⟨divC, divBA⟩ := rel2 with at2
      have t1 := Div5.mul_int with divisible, three
      have t2 := Div5.mul_int with divBA, four
      have t3 := Div5.five with int2b
      have partial := Div5.add with t1, t2
      have combo := Div5.sub with partial, t3
      have same : 3 * (b:R) = (4 * (a:R) + 3 * (b:R)) * 3 + ((b:R) - 3 * (a:R)) * 4 - 5 * (2 * (b:R)) by ring
      have triple := Div5.of_eq with combo, same
      exact nonzero with (Div5.of_three with intB, triple)
    . exact reduced with at3
  exact ⟨newA, newB, int5c, newNonzero, newRelation⟩

theorem step.rotB_transpose (a b c h : Set)
  requires intA : IntReal(a)
  requires intB : IntReal(b)
  requires intC : IntReal(c)
  requires nonzero : ¬Div5(b)
  requires relation : HeadRelation(h, a, b, c)
  requires letter : h ∈ 4
  requires reduced : h ≠ 2
  shows IntReal(3 * (a:R) + 4 * (b:R)) ∧ IntReal(3 * (b:R) - 4 * (a:R)) ∧
    IntReal(5 * (c:R)) ∧ ¬Div5(3 * (b:R) - 4 * (a:R)) ∧
    HeadRelation(3, 3 * (a:R) + 4 * (b:R), 3 * (b:R) - 4 * (a:R), 5 * (c:R))
proof
  have realA := IntReal.real with intA
  have realB := IntReal.real with intB
  have realC := IntReal.real with intC
  have two := IntReal.numeral at 2
  have three := IntReal.numeral at 3
  have four := IntReal.numeral at 4
  have five := IntReal.numeral at 5
  have six := IntReal.numeral at 6
  have int5c := IntReal.mul with five, intC
  have int3a := IntReal.mul with three, intA
  have int4b := IntReal.mul with four, intB
  have int4a := IntReal.mul with four, intA
  have int3b := IntReal.mul with three, intB
  have int2a := IntReal.mul with two, intA
  have newA := IntReal.add with int3a, int4b
  have newB := IntReal.sub with int3b, int4a
  have newRelation : HeadRelation(3, 3 * (a:R) + 4 * (b:R), 3 * (b:R) - 4 * (a:R), 5 * (c:R))
    have divC := Div5.five with intC
    have negative := IntReal.neg with int2a
    have combo := IntReal.sub with negative, intB
    have divCombo := Div5.five with combo
    have same : (3 * (b:R) - 4 * (a:R)) - 2 * (3 * (a:R) + 4 * (b:R)) = 5 * (-(2 * (a:R)) - (b:R)) by ring
    have divB := Div5.of_eq with divCombo, same
    exact HeadRelation.three with divC, divB
  have newNonzero : ¬Div5(3 * (b:R) - 4 * (a:R))
    intro divisible
    obtain ⟨rel0, rel1, rel2, rel3⟩ := relation
    have alternatives := letter.cases with letter
    rcases alternatives with at0 | at1 | at2 | at3
    . obtain ⟨divA, divCB⟩ := rel0 with at0
      have t1 := Div5.mul_int with divA, four
      have sum := Div5.add with divisible, t1
      have same : 3 * (b:R) = (3 * (b:R) - 4 * (a:R)) + (a:R) * 4 by ring
      have triple := Div5.of_eq with sum, same
      exact nonzero with (Div5.of_three with intB, triple)
    . obtain ⟨divA, divCB⟩ := rel1 with at1
      have t1 := Div5.mul_int with divA, four
      have sum := Div5.add with divisible, t1
      have same : 3 * (b:R) = (3 * (b:R) - 4 * (a:R)) + (a:R) * 4 by ring
      have triple := Div5.of_eq with sum, same
      exact nonzero with (Div5.of_three with intB, triple)
    . exact reduced with at2
    . obtain ⟨divC, divBA⟩ := rel3 with at3
      have t1 := Div5.mul_int with divisible, three
      have t2 := Div5.mul_int with divBA, six
      have combo := Div5.sub with t1, t2
      have same : 3 * (b:R) = (3 * (b:R) - 4 * (a:R)) * 3 - ((b:R) - 2 * (a:R)) * 6 by ring
      have triple := Div5.of_eq with combo, same
      exact nonzero with (Div5.of_three with intB, triple)
  exact ⟨newA, newB, int5c, newNonzero, newRelation⟩

-- The basis vectors of ℝ³.
defgraph basis (j : Set) (i ∈ 3) : ℝ :=
  singleValue(Ring.carrier(realRing), Ring.zero(realRing), Ring.one(realRing), j, i)
requires index : j ∈ 3
proof
  have comm := realRing.comm_ring
  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *
  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *
  have closed := singleValue.closed at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), j, i with *
  rw ← realRing.carrierOf
  exact closed

instance basis.vector (j : Set)
  requires index : j ∈ 3
  shows basis(j) : 3 → ℝ
proof
  exact basis.function with index

theorem basis.same (j : Set)
  requires index : j ∈ 3
  shows basis(j)(j) = (1:R)
proof
  have comm := realRing.comm_ring
  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *
  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *
  have same : j = j by rfl
  have value := basis.value at j, j with *
  have selected := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), j, j with zeroIn, oneIn, same
  rw [value, selected, realRing.one_value]
  rfl

theorem basis.other (i j : Set)
  requires row : i ∈ 3
  requires index : j ∈ 3
  requires different : i ≠ j
  shows basis(j)(i) = (0:R)
proof
  have comm := realRing.comm_ring
  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *
  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *
  have value := basis.value at j, i with *
  have selected := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), j, i with zeroIn, oneIn, different
  rw [value, selected, realRing.zero_value]
  rfl

-- The four letters, as Algebra/Group/Words states them.
theorem letterIn.zero
  shows 0 ∈ 4
proof
  exact letter.zero_mem

theorem letterIn.one
  shows 1 ∈ 4
proof
  exact letter.one_mem

theorem letterIn.two
  shows 2 ∈ 4
proof
  exact letter.two_mem

theorem letterIn.three
  shows 3 ∈ 4
proof
  exact letter.three_mem

-- The scaled coordinates along a word: the empty word gives the start
-- vector, and a letter in front acts by five times its matrix.
theorem coordinate.nil (v i : Set)
  requires vector : v : 3 → ℝ
  requires index : i ∈ 3
  shows coordinate([], v, i) = (v(i):R)
proof
  have component := vector.component_real at v, i with *
  rw [coordinate.value, fivePow.nil, wordRotation.nil, matrixVector.one]
  ring

theorem coordinate.cons (ℓ : Set) (rest : List(4)) (v i : Set)
  requires letter : ℓ ∈ 4
  requires vector : v : 3 → ℝ
  requires index : i ∈ 3
  shows coordinate(ℓ :: rest, v, i) =
    (fivePow(rest):R) * (5 * ((letterMatrix(ℓ) · (wordRotation(rest) · v))(i):R))
proof
  have matrix := letterMatrix.matrix with letter
  have inner := matrixVector.vector at wordRotation(rest), v with *
  have outer := matrixVector.vector at letterMatrix(ℓ), wordRotation(rest) · v with *
  have component := vector.component_real at letterMatrix(ℓ) · (wordRotation(rest) · v), i with *
  have scale := fivePow.real at rest
  have law := matrixVector.mul at letterMatrix(ℓ), wordRotation(rest), v with *
  rw [coordinate.value, fivePow.cons, wordRotation.cons, law]
  ring

theorem coordinate.consA (rest : List(4)) (v : Set)
  requires vector : v : 3 → ℝ
  shows coordinate(0 :: rest, v, 0) = 5 * (coordinate(rest, v, 0):R) ∧
    coordinate(0 :: rest, v, 1) = 3 * (coordinate(rest, v, 1):R) - 4 * (coordinate(rest, v, 2):R) ∧
    coordinate(0 :: rest, v, 2) = 4 * (coordinate(rest, v, 1):R) + 3 * (coordinate(rest, v, 2):R)
proof
  have letter := letterIn.zero
  have inner := matrixVector.vector at wordRotation(rest), v with *
  obtain ⟨f0, f1, f2⟩ := rotA.five_action at wordRotation(rest) · v with inner
  have c0 := coordinate.cons at 0, rest, v, 0 with *
  have c1 := coordinate.cons at 0, rest, v, 1 with *
  have c2 := coordinate.cons at 0, rest, v, 2 with *
  have u0 := vector.component_real at wordRotation(rest) · v, 0 with *
  have u1 := vector.component_real at wordRotation(rest) · v, 1 with *
  have u2 := vector.component_real at wordRotation(rest) · v, 2 with *
  have scale := fivePow.real at rest
  constructor
  . rw [c0, letterMatrix.zero, f0, coordinate.value]
    ring
  . constructor
    . rw [c1, letterMatrix.zero, f1, coordinate.value, coordinate.value]
      ring
    . rw [c2, letterMatrix.zero, f2, coordinate.value, coordinate.value]
      ring

theorem coordinate.consAT (rest : List(4)) (v : Set)
  requires vector : v : 3 → ℝ
  shows coordinate(1 :: rest, v, 0) = 5 * (coordinate(rest, v, 0):R) ∧
    coordinate(1 :: rest, v, 1) = 3 * (coordinate(rest, v, 1):R) + 4 * (coordinate(rest, v, 2):R) ∧
    coordinate(1 :: rest, v, 2) = 3 * (coordinate(rest, v, 2):R) - 4 * (coordinate(rest, v, 1):R)
proof
  have letter := letterIn.one
  have inner := matrixVector.vector at wordRotation(rest), v with *
  obtain ⟨f0, f1, f2⟩ := rotA.transpose_five_action at wordRotation(rest) · v with inner
  have c0 := coordinate.cons at 1, rest, v, 0 with *
  have c1 := coordinate.cons at 1, rest, v, 1 with *
  have c2 := coordinate.cons at 1, rest, v, 2 with *
  have u0 := vector.component_real at wordRotation(rest) · v, 0 with *
  have u1 := vector.component_real at wordRotation(rest) · v, 1 with *
  have u2 := vector.component_real at wordRotation(rest) · v, 2 with *
  have scale := fivePow.real at rest
  constructor
  . rw [c0, letterMatrix.one, f0, coordinate.value]
    ring
  . constructor
    . rw [c1, letterMatrix.one, f1, coordinate.value, coordinate.value]
      ring
    . rw [c2, letterMatrix.one, f2, coordinate.value, coordinate.value]
      ring

theorem coordinate.consB (rest : List(4)) (v : Set)
  requires vector : v : 3 → ℝ
  shows coordinate(2 :: rest, v, 0) = 3 * (coordinate(rest, v, 0):R) - 4 * (coordinate(rest, v, 1):R) ∧
    coordinate(2 :: rest, v, 1) = 4 * (coordinate(rest, v, 0):R) + 3 * (coordinate(rest, v, 1):R) ∧
    coordinate(2 :: rest, v, 2) = 5 * (coordinate(rest, v, 2):R)
proof
  have letter := letterIn.two
  have inner := matrixVector.vector at wordRotation(rest), v with *
  obtain ⟨f0, f1, f2⟩ := rotB.five_action at wordRotation(rest) · v with inner
  have c0 := coordinate.cons at 2, rest, v, 0 with *
  have c1 := coordinate.cons at 2, rest, v, 1 with *
  have c2 := coordinate.cons at 2, rest, v, 2 with *
  have u0 := vector.component_real at wordRotation(rest) · v, 0 with *
  have u1 := vector.component_real at wordRotation(rest) · v, 1 with *
  have u2 := vector.component_real at wordRotation(rest) · v, 2 with *
  have scale := fivePow.real at rest
  constructor
  . rw [c0, letterMatrix.two, f0, coordinate.value, coordinate.value]
    ring
  . constructor
    . rw [c1, letterMatrix.two, f1, coordinate.value, coordinate.value]
      ring
    . rw [c2, letterMatrix.two, f2, coordinate.value]
      ring

theorem coordinate.consBT (rest : List(4)) (v : Set)
  requires vector : v : 3 → ℝ
  shows coordinate(3 :: rest, v, 0) = 3 * (coordinate(rest, v, 0):R) + 4 * (coordinate(rest, v, 1):R) ∧
    coordinate(3 :: rest, v, 1) = 3 * (coordinate(rest, v, 1):R) - 4 * (coordinate(rest, v, 0):R) ∧
    coordinate(3 :: rest, v, 2) = 5 * (coordinate(rest, v, 2):R)
proof
  have letter := letterIn.three
  have inner := matrixVector.vector at wordRotation(rest), v with *
  obtain ⟨f0, f1, f2⟩ := rotB.transpose_five_action at wordRotation(rest) · v with inner
  have c0 := coordinate.cons at 3, rest, v, 0 with *
  have c1 := coordinate.cons at 3, rest, v, 1 with *
  have c2 := coordinate.cons at 3, rest, v, 2 with *
  have u0 := vector.component_real at wordRotation(rest) · v, 0 with *
  have u1 := vector.component_real at wordRotation(rest) · v, 1 with *
  have u2 := vector.component_real at wordRotation(rest) · v, 2 with *
  have scale := fivePow.real at rest
  constructor
  . rw [c0, letterMatrix.three, f0, coordinate.value, coordinate.value]
    ring
  . constructor
    . rw [c1, letterMatrix.three, f1, coordinate.value, coordinate.value]
      ring
    . rw [c2, letterMatrix.three, f2, coordinate.value]
      ring

-- Swierczkowski's invariant for the word ℓ :: rest from the start vector
-- v: the scaled coordinates are integers, the middle one is not a
-- multiple of five, and the residues are those forced by the letter ℓ.
predicate Swierczkowski (ℓ rest v : Set) :=
  IntReal(coordinate(ℓ :: rest, v, 0)) ∧ IntReal(coordinate(ℓ :: rest, v, 1)) ∧
  IntReal(coordinate(ℓ :: rest, v, 2)) ∧ ¬Div5(coordinate(ℓ :: rest, v, 1)) ∧
  HeadRelation(ℓ, coordinate(ℓ :: rest, v, 0), coordinate(ℓ :: rest, v, 1),
    coordinate(ℓ :: rest, v, 2))

theorem Swierczkowski.step (ℓ h : Set) (rest : List(4)) (v : Set)
  requires letterL : ℓ ∈ 4
  requires letterH : h ∈ 4
  requires reduced : h ≠ inverseLetter(ℓ)
  requires vector : v : 3 → ℝ
  requires invariant : Swierczkowski(h, rest, v)
  shows Swierczkowski(ℓ, h :: rest, v)
proof
  obtain ⟨intA, intB, intC, nonzero, relation⟩ := invariant
  have alternatives := letter.cases with letterL
  rcases alternatives with at0 | at1 | at2 | at3
  . rw [at0, inverseLetter.zero] at reduced
    rw at0
    obtain ⟨c0, c1, c2⟩ := coordinate.consA at h :: rest, v with vector
    obtain ⟨newA, newB, newC, newNonzero, newRelation⟩ := step.rotA with intA, intB,
      intC, nonzero, relation, letterH, reduced
    unfold Swierczkowski
    rw [c0, c1, c2]
    exact ⟨newA, newB, newC, newNonzero, newRelation⟩
  . rw [at1, inverseLetter.one] at reduced
    rw at1
    obtain ⟨c0, c1, c2⟩ := coordinate.consAT at h :: rest, v with vector
    obtain ⟨newA, newB, newC, newNonzero, newRelation⟩ := step.rotA_transpose with intA,
      intB, intC, nonzero, relation, letterH, reduced
    unfold Swierczkowski
    rw [c0, c1, c2]
    exact ⟨newA, newB, newC, newNonzero, newRelation⟩
  . rw [at2, inverseLetter.two] at reduced
    rw at2
    obtain ⟨c0, c1, c2⟩ := coordinate.consB at h :: rest, v with vector
    obtain ⟨newA, newB, newC, newNonzero, newRelation⟩ := step.rotB with intA, intB,
      intC, nonzero, relation, letterH, reduced
    unfold Swierczkowski
    rw [c0, c1, c2]
    exact ⟨newA, newB, newC, newNonzero, newRelation⟩
  . rw [at3, inverseLetter.three] at reduced
    rw at3
    obtain ⟨c0, c1, c2⟩ := coordinate.consBT at h :: rest, v with vector
    obtain ⟨newA, newB, newC, newNonzero, newRelation⟩ := step.rotB_transpose with intA,
      intB, intC, nonzero, relation, letterH, reduced
    unfold Swierczkowski
    rw [c0, c1, c2]
    exact ⟨newA, newB, newC, newNonzero, newRelation⟩

-- The one-letter words: b and b⁻¹ from (1, 0, 0), a and a⁻¹ from (0, 0, 1).
theorem Swierczkowski.base_b
  shows Swierczkowski(2, [], basis(0))
proof
  have vector := basis.vector at 0 with *
  have e0 := basis.same at 0 with *
  have e1 := basis.other at 1, 0 with index.one_mem, index.zero_mem, index.one_ne_zero
  have e2 := basis.other at 2, 0 with index.two_mem, index.zero_mem, index.two_ne_zero
  obtain ⟨c0, c1, c2⟩ := coordinate.consB at [], basis(0) with vector
  have n0 := coordinate.nil at basis(0), 0 with *
  have n1 := coordinate.nil at basis(0), 1 with *
  have n2 := coordinate.nil at basis(0), 2 with *
  have value0 : coordinate(2 :: [], basis(0), 0) = (3:R)
    rw [c0, n0, n1, e0, e1]
    ring
  have value1 : coordinate(2 :: [], basis(0), 1) = (4:R)
    rw [c1, n0, n1, e0, e1]
    ring
  have value2 : coordinate(2 :: [], basis(0), 2) = (0:R)
    rw [c2, n2, e2]
    ring
  have three := IntReal.numeral at 3
  have four := IntReal.numeral at 4
  have zero := IntReal.zero
  have one := IntReal.one
  have negative := IntReal.sub with zero, one
  have multiple := Div5.five with negative
  have residue : Div5((4:R) - 3 * (3:R))
    have same : (4:R) - 3 * (3:R) = 5 * ((0:R) - (1:R)) by ring
    rw same
    exact multiple
  have relation := HeadRelation.two at (3:R), (4:R), (0:R) with Div5.zero, residue
  unfold Swierczkowski
  rw [value0, value1, value2]
  exact ⟨three, four, zero, Div5.not_four, relation⟩

theorem Swierczkowski.base_bt
  shows Swierczkowski(3, [], basis(0))
proof
  have vector := basis.vector at 0 with *
  have e0 := basis.same at 0 with *
  have e1 := basis.other at 1, 0 with index.one_mem, index.zero_mem, index.one_ne_zero
  have e2 := basis.other at 2, 0 with index.two_mem, index.zero_mem, index.two_ne_zero
  obtain ⟨c0, c1, c2⟩ := coordinate.consBT at [], basis(0) with vector
  have n0 := coordinate.nil at basis(0), 0 with *
  have n1 := coordinate.nil at basis(0), 1 with *
  have n2 := coordinate.nil at basis(0), 2 with *
  have value0 : coordinate(3 :: [], basis(0), 0) = (3:R)
    rw [c0, n0, n1, e0, e1]
    ring
  have value1 : coordinate(3 :: [], basis(0), 1) = (0:R) - 4
    rw [c1, n0, n1, e0, e1]
    ring
  have value2 : coordinate(3 :: [], basis(0), 2) = (0:R)
    rw [c2, n2, e2]
    ring
  have three := IntReal.numeral at 3
  have four := IntReal.numeral at 4
  have zero := IntReal.zero
  have two := IntReal.numeral at 2
  have negativeFour := IntReal.sub with zero, four
  have negativeTwo := IntReal.sub with zero, two
  have multiple := Div5.five with negativeTwo
  have residue : Div5(((0:R) - 4) - 2 * (3:R))
    have same : ((0:R) - 4) - 2 * (3:R) = 5 * ((0:R) - (2:R)) by ring
    rw same
    exact multiple
  have relation := HeadRelation.three at (3:R), (0:R) - 4, (0:R) with Div5.zero, residue
  unfold Swierczkowski
  rw [value0, value1, value2]
  exact ⟨three, negativeFour, zero, Div5.not_neg_four, relation⟩

theorem Swierczkowski.base_a
  shows Swierczkowski(0, [], basis(2))
proof
  have vector := basis.vector at 2 with *
  have e0 := basis.other at 0, 2 with index.zero_mem, index.two_mem, index.zero_ne_two
  have e1 := basis.other at 1, 2 with index.one_mem, index.two_mem, index.one_ne_two
  have e2 := basis.same at 2 with *
  obtain ⟨c0, c1, c2⟩ := coordinate.consA at [], basis(2) with vector
  have n0 := coordinate.nil at basis(2), 0 with *
  have n1 := coordinate.nil at basis(2), 1 with *
  have n2 := coordinate.nil at basis(2), 2 with *
  have value0 : coordinate(0 :: [], basis(2), 0) = (0:R)
    rw [c0, n0, e0]
    ring
  have value1 : coordinate(0 :: [], basis(2), 1) = (0:R) - 4
    rw [c1, n1, n2, e1, e2]
    ring
  have value2 : coordinate(0 :: [], basis(2), 2) = (3:R)
    rw [c2, n1, n2, e1, e2]
    ring
  have three := IntReal.numeral at 3
  have four := IntReal.numeral at 4
  have zero := IntReal.zero
  have negativeFour := IntReal.sub with zero, four
  have multiple := Div5.five with three
  have residue : Div5((3:R) - 3 * ((0:R) - 4))
    have same : (3:R) - 3 * ((0:R) - 4) = 5 * (3:R) by ring
    rw same
    exact multiple
  have relation := HeadRelation.zero at (0:R), (0:R) - 4, (3:R) with Div5.zero, residue
  unfold Swierczkowski
  rw [value0, value1, value2]
  exact ⟨zero, negativeFour, three, Div5.not_neg_four, relation⟩

theorem Swierczkowski.base_at
  shows Swierczkowski(1, [], basis(2))
proof
  have vector := basis.vector at 2 with *
  have e0 := basis.other at 0, 2 with index.zero_mem, index.two_mem, index.zero_ne_two
  have e1 := basis.other at 1, 2 with index.one_mem, index.two_mem, index.one_ne_two
  have e2 := basis.same at 2 with *
  obtain ⟨c0, c1, c2⟩ := coordinate.consAT at [], basis(2) with vector
  have n0 := coordinate.nil at basis(2), 0 with *
  have n1 := coordinate.nil at basis(2), 1 with *
  have n2 := coordinate.nil at basis(2), 2 with *
  have value0 : coordinate(1 :: [], basis(2), 0) = (0:R)
    rw [c0, n0, e0]
    ring
  have value1 : coordinate(1 :: [], basis(2), 1) = (4:R)
    rw [c1, n1, n2, e1, e2]
    ring
  have value2 : coordinate(1 :: [], basis(2), 2) = (3:R)
    rw [c2, n1, n2, e1, e2]
    ring
  have three := IntReal.numeral at 3
  have four := IntReal.numeral at 4
  have zero := IntReal.zero
  have one := IntReal.one
  have negative := IntReal.sub with zero, one
  have multiple := Div5.five with negative
  have residue : Div5((3:R) - 2 * (4:R))
    have same : (3:R) - 2 * (4:R) = 5 * ((0:R) - (1:R)) by ring
    rw same
    exact multiple
  have relation := HeadRelation.one at (0:R), (4:R), (3:R) with Div5.zero, residue
  unfold Swierczkowski
  rw [value0, value1, value2]
  exact ⟨zero, four, three, Div5.not_four, relation⟩

-- Along a reduced word ending in the letter x, the invariant from a start
-- vector adapted to x holds with the word's first letter.
theorem Swierczkowski.of_last (w : List(4)) (x v : Set)
  requires letter : x ∈ 4
  requires vector : v : 3 → ℝ
  requires base : Swierczkowski(x, [], v)
  requires reduced : Reduced(w)
  requires shape : ∃ u, List(4, u) ∧ w = append{A := 4}(x :: [], u)
  shows ∃ ℓ ∈ 4, ∃ rest, List(4, rest) ∧ w = ℓ :: rest ∧ Swierczkowski(ℓ, rest, v)
proof
  induction w
  | List.nil =>
    intros reduced shape
    obtain ⟨u, listU, equal⟩ := shape
    symm at equal
    have parts := append.nil_iff.forward with equal
    have distinct := List.cons_ne_nil at 4, x, [] with letter
    exfalso
    exact distinct with parts.right
  | List.cons(ℓ, rest) using ih =>
    intros reduced shape
    have letterL : ℓ ∈ 4 by assumption
    have listRest : List(4, rest) by assumption
    obtain ⟨u, listU, equal⟩ := shape
    have cases := List.cases at 4, u with listU
    cases cases with empty | consU
    . have single : List(4, x :: []) by typecheck
      have nilCase := append.nil at 4, x :: [] with single
      rw [empty, nilCase] at equal
      have both := List.cons_injective at 4, ℓ, x, rest, [] with letterL, letter, equal
      obtain ⟨headEq, tailEq⟩ := both
      refine ⟨ℓ, letterL, rest, listRest, rfl, ?_⟩
      rw [headEq, tailEq]
      exact base
    . obtain ⟨y, letterY, tail, listTail, shapeU⟩ := consU
      have single : List(4, x :: []) by typecheck
      have consCase := append.cons at 4, y, tail, x :: [] with letterY
      rw [shapeU, consCase] at equal
      have both := List.cons_injective at 4, ℓ, y, rest, append{A := 4}(x :: [], tail)
        with letterL, letterY, equal
      obtain ⟨headEq, tailEq⟩ := both
      have reducedRest := Reduced.tail at ℓ, rest with letterL, reduced
      have shapeRest : ∃ u, List(4, u) ∧ rest = append{A := 4}(x :: [], u)
        exact ⟨tail, listTail, tailEq⟩
      obtain ⟨h, letterH, rest2, listRest2, shapeRest2, invariant⟩ := ih with reducedRest,
        shapeRest
      rw shapeRest2 at reduced
      have criterion := Reduced.cons_cons.forward at ℓ, h, rest2 with letterL, letterH, reduced
      have notInverse := cancels.false_iff.forward with criterion.left
      have stepped := Swierczkowski.step with letterL, letterH, notInverse, vector, invariant
      refine ⟨ℓ, letterL, h :: rest2, ?_, ?_, stepped⟩
      . typecheck
      . rw shapeRest2
        rfl

-- The freeness theorem: a nonempty reduced word is not the identity.
theorem wordRotation.ne_one (w : List(4))
  requires reduced : Reduced(w)
  requires nonempty : w ≠ []
  shows wordRotation(w) ≠ Ring.one(matrixRing(realRing, 3))
proof
  intro trivial
  have shape := List.snoc_cases at 4, w with *
  cases shape with empty | snoc
  . exact nonempty with empty
  . obtain ⟨x, letter, front, listFront, equal⟩ := snoc
    have finish : ∀ v, (v : 3 → ℝ) → v(1) = (0:R) → Swierczkowski(x, [], v) → ⊥
      intros v vector zero base
      have shapeW : ∃ u, List(4, u) ∧ w = append{A := 4}(x :: [], u)
        exact ⟨front, listFront, equal⟩
      obtain ⟨ℓ, letterL, rest, listRest, split, invariant⟩ := Swierczkowski.of_last at w, x, v
        with letter, vector, base, reduced, shapeW
      obtain ⟨intA, intB, intC, nonzero, relation⟩ := invariant
      have scale := fivePow.real at w
      have value : coordinate(ℓ :: rest, v, 1) = (0:R)
        rw [coordinate.value, ← split, trivial, matrixVector.one, zero]
        ring
      apply nonzero
      rw value
      exact Div5.zero
    have alternatives := letter.cases with letter
    rcases alternatives with at0 | at1 | at2 | at3
    . have vector := basis.vector at 2 with *
      have zero := basis.other at 1, 2 with index.one_mem, index.two_mem, index.one_ne_two
      have target := finish with basis(2), vector, zero
      rw at0 at target
      exact target with Swierczkowski.base_a
    . have vector := basis.vector at 2 with *
      have zero := basis.other at 1, 2 with index.one_mem, index.two_mem, index.one_ne_two
      have target := finish with basis(2), vector, zero
      rw at1 at target
      exact target with Swierczkowski.base_at
    . have vector := basis.vector at 0 with *
      have zero := basis.other at 1, 0 with index.one_mem, index.zero_mem, index.one_ne_zero
      have target := finish with basis(0), vector, zero
      rw at2 at target
      exact target with Swierczkowski.base_b
    . have vector := basis.vector at 0 with *
      have zero := basis.other at 1, 0 with index.one_mem, index.zero_mem, index.one_ne_zero
      have target := finish with basis(0), vector, zero
      rw at3 at target
      exact target with Swierczkowski.base_bt

theorem wordRotation.ne_unit (w : List(4))
  requires reduced : Reduced(w)
  requires nonempty : w ≠ []
  shows wordRotation(w) ≠ Group.one(SO3)
proof
  rw SO3.oneOf
  exact wordRotation.ne_one with reduced, nonempty

-- The word ab is not the identity.
theorem wordRotation.sample
  shows wordRotation(0 :: 2 :: []) ≠ Ring.one(matrixRing(realRing, 3))
proof
  have reduced : Reduced(0 :: 2 :: [])
    unfold Reduced
    compute
  have nonempty : 0 :: 2 :: [] ≠ []
    have tail := List.closed_cons at 4, 2, [] with letterIn.two
    exact List.cons_ne_nil at 4, 0, 2 :: [] with tail, letterIn.zero
  have tail := List.closed_cons at 4, 2, [] with letterIn.two
  have word := List.closed_cons at 4, 0, 2 :: [] with tail, letterIn.zero
  exact wordRotation.ne_one with word, reduced, nonempty