LeanPool.Rupert.Tetrahedron

Imported Lean Pool material for LeanPool.Rupert.Tetrahedron.

def Tetrahedron.vertices : Fin 4 → ℝ³

Vertices of a regular tetrahedron.

Equations

• Tetrahedron.vertices = ![!₂[1, 1, 1], !₂[1, -1, -1], !₂[-1, 1, -1], !₂[-1, -1, 1]]

def Tetrahedron.outerQuat : Quaternion ℝ

Quaternion certificate for the outer tetrahedron rotation.

Equations

• Tetrahedron.outerQuat = { re := 0.338990, imI := -0.426182, imJ := 0.173602, imK := -0.820558 }

noncomputable def Tetrahedron.outerRot : Matrix (Fin 3) (Fin 3) ℝ

Rotation matrix for the outer tetrahedron.

Equations

• Tetrahedron.outerRot = matrixOfQuat Tetrahedron.outerQuat

theorem Tetrahedron.outerRot_so3 : outerRot ∈ SO3

def Tetrahedron.innerQuat : Quaternion ℝ

Quaternion certificate for the inner tetrahedron rotation.

Equations

• Tetrahedron.innerQuat = { re := 0.857701, imI := -0.119161, imJ := 0.443971, imK := 0.230299 }

noncomputable def Tetrahedron.innerRot : Matrix (Fin 3) (Fin 3) ℝ

Rotation matrix for the inner tetrahedron.

Equations

• Tetrahedron.innerRot = matrixOfQuat Tetrahedron.innerQuat

theorem Tetrahedron.innerRot_so3 : innerRot ∈ SO3

def Tetrahedron.innerOffset : ℝ²

Translation offset for the inner tetrahedron shadow.

Equations

• Tetrahedron.innerOffset = !₂[98412e-6, -0.165800]

theorem Tetrahedron.rupert : IsRupert vertices