Is Every Convex Polyhedron Rupert?

A polyhedron is Rupert if one can cut a hole in it and pass another copy of the same polyhedron through that hole.

More formally: a convex body in ℝ³ is a compact, convex set with nonempty interior. A convex body X is said to be Rupert if there are two affine transforms T₁, T₂ ∈ SE(3) such that π(T₁(X)) ⊆ int(π(T₂(X))), where π : ℝ³ → ℝ² is the evident projection, and int denotes topological interior.

Not all convex bodies are Rupert. For example,

• the unit ball is not Rupert
• the circular cylinder of unit diameter and height closed on each end by disks is not Rupert

However, many convex polyhedra are Rupert. All Platonic solids, and most Archimedean and Catalan solids are known to be Rupert.

Question: are all convex polyhedra with nonempty interior Rupert?

References:

• Platonic Passages, R. P. Jerrard, J. E. Wetzel, and L. Yuan., Math. Mag., 90(2):87–98, 2017. conjectures ("with a certain hesitancy") that perhaps all convex polyhedra are Rupert.

• However, An Algorithmic Approach to Rupert's Problem describes experimental evidence to suggest that three Archimedean solids may not be Rupert.

• Optimizing for the Rupert property is the source of some of the Catalan solid results, and has more results for Johnson polyhedra as well.

• This video by David Renshaw visualizes known results for Platonic, Archimedean, and Catalan solids.

• This problem's name comes from the fact that it is a generalization of Prince Rupert's Cube.

@[reducible, inline]

abbrev Rupert.SO3 : Submonoid (Matrix (Fin 3) (Fin 3) ℝ)

Equations

• Rupert.SO3 = Matrix.specialOrthogonalGroup (Fin 3) ℝ

def Rupert.«termℝ²» : Lean.ParserDescr

Equations

• Rupert.«termℝ²» = Lean.ParserDescr.node `Rupert.«termℝ²» 1024 (Lean.ParserDescr.symbol "ℝ²")

def Rupert.«termℝ³» : Lean.ParserDescr

Equations

• Rupert.«termℝ³» = Lean.ParserDescr.node `Rupert.«termℝ³» 1024 (Lean.ParserDescr.symbol "ℝ³")

def Rupert.transformed_shadow (X : Set (Fin 3 → ℝ)) (offset : Fin 2 → ℝ) (rotation : ↥SO3) : Set (Fin 2 → ℝ)

The result of transforming a subset of ℝ³ by a chosen rotation and offset, and then projected to ℝ².

Equations

• Rupert.transformed_shadow X offset rotation = (fun (p : Fin 3 → ℝ) => offset + (↑rotation).mulVec p ∘ Fin.castSucc) '' X

def Rupert.IsRupert (vertices : Finset (Fin 3 → ℝ)) : Prop

A convex polyhedron (given as a finite collection of vertices) is Rupert if there are two rotations in ℝ³ (called "inner" and "outer") and a translation in ℝ² such that the "inner shadow" (the projection to ℝ² of the inner rotation applied to the polyhedron, then translated) fits in the interior of the "outer shadow" (the projection to ℝ² of the outer rotation applied to the polyhedron)

[Note: The restriction to (polyhedra determined by the convex hulls of) finite sets of vertices here is deliberate. Were we to generalize to arbitrary subsets of ℝⁿ we'd probably want to make the containment relation more strict, e.g. closure inner_shadow ⊆ interior outer_shadow to rule out, e.g. the open ball being Rupert. However, we didn't observe any such generalization in the literature yet, so we stuck to what was in the citations above.]

Equations

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

theorem Rupert.is_every_convex_polyhedron_rupert : (∀ (vertices : Finset (Fin 3 → ℝ)), (interior ((convexHull ℝ) ↑vertices)).Nonempty → IsRupert vertices) ↔ sorry

Does the Rupert property hold for every convex polyhedron with nonempty interior?