Exact data for the Cayley checker

Dyadic approximations (error at most 2⁻⁶⁰ per coordinate) of the Noperthedron vertices and of the symmetry rotations Rz(2πk/15), the half-turn τ data, and the paired vertices of the blown-up charts. Mathlib-free.

structure Cayley.V3 (α : Type) : Type

Three-vectors.

• x : α
• y : α
• z : α

@[instance_reducible]

instance Cayley.instInhabitedV3 {a✝ : Type} [Inhabited a✝] : Inhabited (V3 a✝)

Equations

• Cayley.instInhabitedV3 = { default := Cayley.instInhabitedV3.default }

structure Cayley.M3 (α : Type) : Type

3×3 matrices, stored by entries so that compiled code never recomputes them.

• a00 : α
• a01 : α
• a02 : α
• a10 : α
• a11 : α
• a12 : α
• a20 : α
• a21 : α
• a22 : α

@[instance_reducible]

instance Cayley.instInhabitedM3 {a✝ : Type} [Inhabited a✝] : Inhabited (M3 a✝)

Equations

• Cayley.instInhabitedM3 = { default := Cayley.instInhabitedM3.default }

def Cayley.d80 (m : Int) : QI

The dyadic number m · 2⁻⁸⁰.

Equations

• Cayley.d80 m = { m := m, e := 80 }

def Cayley.cosTab : Array QI

cos(2πk/15) to within 2⁻⁸⁰.

Equations

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

def Cayley.sinTab : Array QI

sin(2πk/15) to within 2⁻⁸⁰.

Equations

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

def Cayley.cTab : Array (V3 QI)

The points C1, C2, C3 to within 2⁻⁸⁰.

Equations

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

def Cayley.vertexOf (k l i : Nat) : V3 QI

Vertex 6k + 3ℓ + i is (-1)^ℓ Rz(2πk/15) C_i.

Equations

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

def Cayley.vertexTab : Array (V3 QI)

Equations

• Cayley.vertexTab = Array.map (fun (j : Nat) => Cayley.vertexOf (j / 6) (j % 6 / 3) (j % 3)) (Array.range 90)

def Cayley.groupTab : Array (M3 QI)

Rz(2πk/15) approximately.

Equations

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

def Cayley.c3x : Int

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

Equations

• Cayley.c3x = 8193990033

def Cayley.c3y : Int

Equations

• Cayley.c3y = 5298215096

def Cayley.kappaTau : Int

The denominator κ = x'² + y'² of the half-turn τ.

Equations

• Cayley.kappaTau = Cayley.c3x * Cayley.c3x + Cayley.c3y * Cayley.c3y

def Cayley.tauPair (j : Nat) : Option Nat

The vertex that τ maps vertex j to, for the 30 copies of C3.

Equations

• Cayley.tauPair j = if j % 3 = 2 then have k := j / 6; have l := j % 6 / 3; some (6 * ((15 - k) % 15) + 3 * (1 - l) + 2) else none

def Cayley.pairOf (chart j : Nat) : Option Nat

The paired vertex for the blown-up charts.

Equations

• Cayley.pairOf chart j = if chart = 0 then some j else if chart = 4 then Cayley.tauPair j else none

def Cayley.errε : QI

Componentwise error bound ε = 2⁻⁶⁰ of the approximations.

Equations

• Cayley.errε = { m := 1, e := 60 }