Reduced poses in Cayley coordinates

The outer rotation is s(u, v) = Cay(v, -u, 0); the inner rotation is s(u, v) · B_j · Cay(r) for a chart base B_j. Reduced u v j r collects the inequalities that the reduction (Cayley.Soundness.Reduction) guarantees.

noncomputable def Cayley.outerRot (u v : ℝ) : Matrix (Fin 3) (Fin 3) ℝ

The outer rotation with stereographic view coordinates (u, v).

Equations

• Cayley.outerRot u v = Cayley.cayleyMatrix v (-u) 0

noncomputable def Cayley.cayV (r : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 3) ℝ

The Cayley rotation of a vector.

Equations

• Cayley.cayV r = Cayley.cayleyMatrix (r 0) (r 1) (r 2)

def Cayley.c3xR : ℝ

C3 = (x', y', ·) · 10⁻¹⁰.

Equations

• Cayley.c3xR = 8193990033

def Cayley.c3yR : ℝ

Equations

• Cayley.c3yR = 5298215096

def Cayley.kapR : ℝ

Equations

• Cayley.kapR = Cayley.c3xR ^ 2 + Cayley.c3yR ^ 2

noncomputable def Cayley.tauR : Matrix (Fin 3) (Fin 3) ℝ

τ: minus the reflection in the vertical plane through C3.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Cayley.chartB : ℕ → Matrix (Fin 3) (Fin 3) ℝ

The chart bases: the Klein four-group and τ.

Equations

• Cayley.chartB 0 = !![1, 0, 0; 0, 1, 0; 0, 0, 1]
• Cayley.chartB 1 = !![1, 0, 0; 0, -1, 0; 0, 0, -1]
• Cayley.chartB 2 = !![-1, 0, 0; 0, 1, 0; 0, 0, -1]
• Cayley.chartB 3 = !![-1, 0, 0; 0, -1, 0; 0, 0, 1]
• Cayley.chartB x✝ = Cayley.tauR

def Cayley.ZR : Matrix (Fin 3) (Fin 3) ℝ

The screen half-turn Rz(π).

Equations

• Cayley.ZR = !![-1, 0, 0; 0, -1, 0; 0, 0, 1]

noncomputable def Cayley.Hmat (u v : ℝ) : Matrix (Fin 3) (Fin 3) ℝ

The half-turn about the outer view, sᵀ Rz(π) s.

Equations

• Cayley.Hmat u v = (Cayley.outerRot u v).transpose * Cayley.ZR * Cayley.outerRot u v

noncomputable def Cayley.Fsc (X : Matrix (Fin 3) (Fin 3) ℝ) : ℝ

The orbit score F(X) = max(tr X, tr(τᵀX) − 1/8).

Equations

• Cayley.Fsc X = max X.trace ((Cayley.tauR.transpose * X).trace - 1 / 8)

noncomputable def Cayley.Qm (j : ℕ) (r : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 3) ℝ

The relative rotation in chart j.

Equations

• Cayley.Qm j r = Cayley.chartB j * Cayley.cayV r

structure Cayley.Reduced (u v : ℝ) (j : ℕ) (r : Fin 3 → ℝ) : Prop

The reduced domain.

• j_lt : j < 5
• u_nonneg : 0 ≤ u
• v_nonneg : 0 ≤ v
• wedge : v ≤ 57 / 128 * u
• disk : u ^ 2 + v ^ 2 ≤ 1
• chart (k : ℕ) : k < 5 → ((chartB k).transpose * Qm j r).trace ≤ ((chartB j).transpose * Qm j r).trace
• orbit (e : Bool) (k : ℕ) : Fsc ((if e = true then Hmat u v else 1) * Qm j r * gR k) ≤ Fsc (Qm j r)
• rb (i : Fin 3) : |r i| ≤ if j = 4 then 2 else 1

Orthogonality

theorem Cayley.mem_SO3_iff' (A : Matrix (Fin 3) (Fin 3) ℝ) : A ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ ↔ A * A.transpose = 1 ∧ A.det = 1

theorem Cayley.tauR_mem_SO3 : tauR ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ

theorem Cayley.chartB_mem_SO3 (j : ℕ) : chartB j ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ

theorem Cayley.ZR_eq : ZR = Rz_mat Real.pi

theorem Cayley.outerRot_mem_SO3 (u v : ℝ) : outerRot u v ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ

theorem Cayley.cayV_mem_SO3 (r : Fin 3 → ℝ) : cayV r ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ

theorem Cayley.SO3_mul_transpose {A : Matrix (Fin 3) (Fin 3) ℝ} (h : A ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) : A * A.transpose = 1

theorem Cayley.SO3_transpose_mul {A : Matrix (Fin 3) (Fin 3) ℝ} (h : A ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) : A.transpose * A = 1