The reduction to a reduced Cayley pose

Every Rupert pair of rotations yields a Rupert pair (s(u,v), s(u,v) · B_j · Cay(r)) with Reduced u v j r. See cayley/DESIGN.md, steps A–C.

Step A: the outer view

theorem Cayley.RxPi_mem_SO3 : RxPi ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ

theorem Cayley.gR_mem_SO3 (k : ℕ) : gR k ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ

theorem Cayley.step_flip {Ro Ri : Matrix (Fin 3) (Fin 3) ℝ} (hRo : Ro ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) (hRi : Ri ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) (h : RupPair Ro Ri) : ∃ Ro' ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ, ∃ Ri' ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ, RupPair Ro' Ri' ∧ 0 ≤ Ro' 2 2

theorem Cayley.gR_eq (k : ℕ) : gR k = Rz_mat (↑k * θ₁)

theorem Cayley.mul_gR_row2 (R : Matrix (Fin 3) (Fin 3) ℝ) (k : ℕ) : (R * gR k) 2 0 = R 2 0 * Real.cos (↑k * θ₁) + R 2 1 * Real.sin (↑k * θ₁) ∧ (R * gR k) 2 1 = -R 2 0 * Real.sin (↑k * θ₁) + R 2 1 * Real.cos (↑k * θ₁) ∧ (R * gR k) 2 2 = R 2 2

theorem Cayley.step_azimuth (a b : ℝ) : ∃ (k : ℕ), 0 ≤ a * Real.cos (↑k * θ₁) + b * Real.sin (↑k * θ₁) ∧ 0 ≤ -a * Real.sin (↑k * θ₁) + b * Real.cos (↑k * θ₁) ∧ -a * Real.sin (↑k * θ₁) + b * Real.cos (↑k * θ₁) ≤ 57 / 128 * (a * Real.cos (↑k * θ₁) + b * Real.sin (↑k * θ₁))

theorem Cayley.outerRot_row2 (u v : ℝ) : outerRot u v 2 0 = 2 * u / (1 + u ^ 2 + v ^ 2) ∧ outerRot u v 2 1 = 2 * v / (1 + u ^ 2 + v ^ 2) ∧ outerRot u v 2 2 = (1 - u ^ 2 - v ^ 2) / (1 + u ^ 2 + v ^ 2)

theorem Cayley.eq_Rz_mul_outerRot (R : Matrix (Fin 3) (Fin 3) ℝ) (hR : R ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) (u v : ℝ) (h0 : R 2 0 = outerRot u v 2 0) (h1 : R 2 1 = outerRot u v 2 1) (h2 : R 2 2 = outerRot u v 2 2) : ∃ (γ : ℝ), R = Rz_mat γ * outerRot u v

An SO(3) matrix whose third row is the stereographic image of (u, v) is Rz(γ) · s(u, v).

theorem Cayley.step_outer {Ro Ri : Matrix (Fin 3) (Fin 3) ℝ} (hRo : Ro ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) (hRi : Ri ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) (h : RupPair Ro Ri) : ∃ (u : ℝ) (v : ℝ), 0 ≤ u ∧ 0 ≤ v ∧ v ≤ 57 / 128 * u ∧ u ^ 2 + v ^ 2 ≤ 1 ∧ ∃ Ri' ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ, RupPair (outerRot u v) Ri'

Step A: a Rupert pair with outer rotation s(u, v) in the wedge.

Step B: the relative rotation's orbit

theorem Cayley.gR_mul (k k' : ℕ) : gR k * gR k' = gR (k + k')

theorem Cayley.gR_mod (k : ℕ) : gR (k % 15) = gR k

theorem Cayley.ZR_mul_self : ZR * ZR = 1

theorem Cayley.Hmat_mul_self (u v : ℝ) : Hmat u v * Hmat u v = 1

noncomputable def Cayley.hp (u v : ℝ) (e : Bool) : Matrix (Fin 3) (Fin 3) ℝ

H^e.

Equations

• Cayley.hp u v e = if e = true then Cayley.Hmat u v else 1

theorem Cayley.hp_mul (u v : ℝ) (e e' : Bool) : hp u v e' * hp u v e = hp u v (e ^^ e')

theorem Cayley.step_orbit {u v : ℝ} {Ri : Matrix (Fin 3) (Fin 3) ℝ} (hRi : Ri ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) (h : RupPair (outerRot u v) Ri) : ∃ Ri' ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ, RupPair (outerRot u v) Ri' ∧ ∀ (e : Bool) (k : ℕ), Fsc (hp u v e * ((outerRot u v).transpose * Ri') * gR k) ≤ Fsc ((outerRot u v).transpose * Ri')

Step C: the chart

theorem Cayley.chartB_transpose_mul_self (j : ℕ) : (chartB j).transpose * chartB j = 1

theorem Cayley.klein_trace_sum (X : Matrix (Fin 3) (Fin 3) ℝ) : ((chartB 0).transpose * X).trace + ((chartB 1).transpose * X).trace + ((chartB 2).transpose * X).trace + ((chartB 3).transpose * X).trace = 0

theorem Cayley.klein_mul (j m : ℕ) (hj : j < 4) (hm : m < 4) (X : Matrix (Fin 3) (Fin 3) ℝ) : (chartB (j ^^^ m)).transpose * (chartB j * X) = chartB m * X

theorem Cayley.trace_diag_mul_cay (a b c x y z : ℝ) : (!![a, 0, 0; 0, b, 0; 0, 0, c] * cayleyMatrix x y z).trace = (a * (1 + x ^ 2 - y ^ 2 - z ^ 2) + b * (1 - x ^ 2 + y ^ 2 - z ^ 2) + c * (1 - x ^ 2 - y ^ 2 + z ^ 2)) / cayleyDenom x y z

theorem Cayley.step_chart (Q : Matrix (Fin 3) (Fin 3) ℝ) (hQ : Q ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) : ∃ j < 5, ∃ (r : Fin 3 → ℝ), Q = Qm j r ∧ (∀ k < 5, ((chartB k).transpose * Q).trace ≤ ((chartB j).transpose * Q).trace) ∧ ∀ (i : Fin 3), |r i| ≤ if j = 4 then 2 else 1

The reduction

theorem Cayley.reduction (h : IsRupert Noperthedron.exactVerts) : ∃ (u : ℝ) (v : ℝ) (j : ℕ) (r : Fin 3 → ℝ), Reduced u v j r ∧ RupPair (outerRot u v) (outerRot u v * Qm j r)