The checker's approximate data

The checker's vertex table is within ε = 2⁻⁶⁰ of the true vertices, its symmetry table within ε of the true rotations, and τ permutes the C3 copies exactly as tauPair says.

def Cayley.vIdx (t : ℕ) : Noperthedron.VertexIndex

The vertex with checker index t = 6k + 3ℓ + i.

Equations

• Cayley.vIdx t = { k := ⟨t / 6 % 15, ⋯⟩, ℓ := ⟨t % 6 / 3, ⋯⟩, i := ⟨t % 3, ⋯⟩ }

noncomputable def Cayley.vtx (t : ℕ) : Fin 3 → ℝ

The true vertex with checker index t.

Equations

• Cayley.vtx t = (Noperthedron.exactVertex (Cayley.vIdx t)).ofLp

theorem Cayley.vIdx_surj (T : Noperthedron.VertexIndex) : ∃ t < 90, vIdx t = T

theorem Cayley.rot_err {c s ch sh x y xh yh e e' : ℝ} (hc : |c - ch| ≤ e) (hs : |s - sh| ≤ e) (hx : |x - xh| ≤ e') (hy : |y - yh| ≤ e') (hcb : |c| ≤ 1) (hsb : |s| ≤ 1) (hxb : |xh| ≤ 1) (hyb : |yh| ≤ 1) : |c * x - s * y - (ch * xh - sh * yh)| ≤ 2 * (e + e') ∧ |s * x + c * y - (sh * xh + ch * yh)| ≤ 2 * (e + e')

Products of approximations.

theorem Cayley.cTab_err (i : ℕ) (hi : i < 3) : |(Noperthedron.Cpt ⟨i, hi⟩).ofLp 0 - D cTab[i]!.x| ≤ 1 / 2 ^ 80 ∧ |(Noperthedron.Cpt ⟨i, hi⟩).ofLp 1 - D cTab[i]!.y| ≤ 1 / 2 ^ 80 ∧ |(Noperthedron.Cpt ⟨i, hi⟩).ofLp 2 - D cTab[i]!.z| ≤ 1 / 2 ^ 80 ∧ |D cTab[i]!.x| ≤ 1 ∧ |D cTab[i]!.y| ≤ 1

theorem Cayley.vertex_approx (t : ℕ) (ht : t < 90) (i : Fin 3) : |vtx t i - vertexTab[t]!.toR i| ≤ D errε

theorem Cayley.cos_sin_reflect (k : ℕ) (hk : k < 15) : Real.cos (2 * Real.pi * ↑((15 - k) % 15) / 15) = Real.cos (2 * Real.pi * ↑k / 15) ∧ Real.sin (2 * Real.pi * ↑((15 - k) % 15) / 15) = -Real.sin (2 * Real.pi * ↑k / 15)

theorem Cayley.tau_pair (s t : ℕ) (hs : s < 90) (h : tauPair s = some t) : vtx t = tauR.mulVec (vtx s)

theorem Cayley.group_approx (g : ℕ) (hg : g < 15) (i k : Fin 3) : |gR g i k - groupTab[g]!.toR i k| ≤ D errε