Moves that preserve Rupert pairs

• a common left factor acting on the screen by a linear homeomorphism (Rz(γ), and Rx(π) which reflects the screen);
• right multiplication of either rotation by a symmetry Rz(2πk/15);
• left multiplication of the inner rotation by Rz(π) (point symmetry).

theorem Cayley.shadow_left (L R : Matrix (Fin 3) (Fin 3) ℝ) (A : Euc(2) ≃L[ℝ] Euc(2)) (hA : ∀ (x : Euc(3)), proj_xyL ((Matrix.toEuclideanLin L) x) = A (proj_xyL x)) : shadow (L * R) = ⇑A '' shadow R

theorem Cayley.rupPair_left {Ro Ri : Matrix (Fin 3) (Fin 3) ℝ} (L : Matrix (Fin 3) (Fin 3) ℝ) (A : Euc(2) ≃L[ℝ] Euc(2)) (hA : ∀ (x : Euc(3)), proj_xyL ((Matrix.toEuclideanLin L) x) = A (proj_xyL x)) (h : RupPair Ro Ri) : RupPair (L * Ro) (L * Ri)

theorem Cayley.rupPair_Rz (γ : ℝ) {Ro Ri : Matrix (Fin 3) (Fin 3) ℝ} (h : RupPair Ro Ri) : RupPair (Rz_mat γ * Ro) (Rz_mat γ * Ri)

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

The half-turn about the x-axis.

Equations

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

noncomputable def Cayley.screenRefl : Euc(2) →L[ℝ] Euc(2)

The reflection (a, b) ↦ (a, -b) of the screen.

Equations

• Cayley.screenRefl = LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin !![1, 0; 0, -1])

theorem Cayley.screenRefl_apply (z : Euc(2)) : screenRefl z = !₂[z.ofLp 0, -z.ofLp 1]

noncomputable def Cayley.screenReflEquiv : Euc(2) ≃L[ℝ] Euc(2)

Equations

• Cayley.screenReflEquiv = ContinuousLinearEquiv.equivOfInverse Cayley.screenRefl Cayley.screenRefl ⋯ ⋯

theorem Cayley.rupPair_RxPi {Ro Ri : Matrix (Fin 3) (Fin 3) ℝ} (h : RupPair Ro Ri) : RupPair (RxPi * Ro) (RxPi * Ri)

Symmetries of the Noperthedron

noncomputable def Cayley.gR (k : ℕ) : Matrix (Fin 3) (Fin 3) ℝ

The symmetry rotation g_k = Rz(2πk/15).

Equations

• Cayley.gR k = Rz_mat (2 * Real.pi * ↑k / 15)

theorem Cayley.RzL_add_apply (α β : ℝ) (v : Euc(3)) : (RzL (α + β)) v = (RzL α) ((RzL β) v)

theorem Cayley.RzL_nat_mod_15 (x : ℕ) : RzL (2 * Real.pi * ↑(x % 15) / 15) = RzL (2 * Real.pi * ↑x / 15)

theorem Cayley.gR_exactVertex (m : ℕ) (T : Noperthedron.VertexIndex) : (Matrix.toEuclideanLin (gR m)) (Noperthedron.exactVertex T) = Noperthedron.exactVertex { k := ⟨(↑T.k + m) % 15, ⋯⟩, ℓ := T.ℓ, i := T.i }

theorem Cayley.gR_image_hull (m : ℕ) : ⇑(Matrix.toEuclideanLin (gR m)) '' Noperthedron.exactHull = Noperthedron.exactHull

theorem Cayley.shadow_mul_gR (R : Matrix (Fin 3) (Fin 3) ℝ) (m : ℕ) : shadow (R * gR m) = shadow R

theorem Cayley.shadow_RzPi_mul (R : Matrix (Fin 3) (Fin 3) ℝ) : shadow (Rz_mat Real.pi * R) = shadow R

Rz(π) negates the screen, and the shadow is centrally symmetric.

theorem Cayley.rupPair_inner_gR {Ro Ri : Matrix (Fin 3) (Fin 3) ℝ} (m : ℕ) (h : RupPair Ro Ri) : RupPair Ro (Ri * gR m)

theorem Cayley.rupPair_outer_gR {Ro Ri : Matrix (Fin 3) (Fin 3) ℝ} (m : ℕ) (h : RupPair Ro Ri) : RupPair (Ro * gR m) Ri

theorem Cayley.rupPair_inner_RzPi {Ro Ri : Matrix (Fin 3) (Fin 3) ℝ} (h : RupPair Ro Ri) : RupPair Ro (Rz_mat Real.pi * Ri)