LeanPool.Rupert.TriakisTetrahedron

Imported Lean Pool material for LeanPool.Rupert.TriakisTetrahedron.

noncomputable def TriakisTetrahedron.vertices : Fin 8 → ℝ³

Vertices of tom7's triakis tetrahedron, scaled by 3 / 5.

Equations

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

def TriakisTetrahedron.innerQuat : Quaternion ℝ

Quaternion certificate for the inner rotation.

Equations

• TriakisTetrahedron.innerQuat = { re := 0.144873924, imI := 0.365747659, imJ := -0.854692880, imK := -0.338733344 }

def TriakisTetrahedron.innerOffset : ℝ²

Translation offset for the inner shadow.

Equations

• TriakisTetrahedron.innerOffset = !₂[85629464761e-15, 89387250451e-15]

def TriakisTetrahedron.outerQuat : Quaternion ℝ

Quaternion certificate for the outer rotation.

Equations

• TriakisTetrahedron.outerQuat = { re := 0.858732110, imI := -0.148912807, imJ := -0.352436516, imK := -0.340870417 }

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

Rotation matrix for the inner triakis tetrahedron.

Equations

• TriakisTetrahedron.innerRot = matrixOfQuat TriakisTetrahedron.innerQuat

theorem TriakisTetrahedron.innerRot_so3 : innerRot ∈ SO3

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

Rotation matrix for the outer triakis tetrahedron.

Equations

• TriakisTetrahedron.outerRot = matrixOfQuat TriakisTetrahedron.outerQuat

theorem TriakisTetrahedron.outerRot_so3 : outerRot ∈ SO3

theorem TriakisTetrahedron.outer_ball_subset : Metric.ball 0 6e-3 ⊆ (convexHull ℝ) {x : ℝ² | ∃ (i : Fin 8), projXy ((Matrix.toEuclideanLin outerRot) (vertices i)) = x}

theorem TriakisTetrahedron.rupert : IsRupert vertices