Rupert.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

4 declarations, 1 contain sorry, 0 declared as axioms

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.
A convex polyhedron without Rupert's property, Jakob Steininger and Sergey Yurkevich, 2025. Constructs a convex polyhedron and a proof that it is not Rupert, resolving the open question.

Imports (1)

FormalConjecturesUtil

abbrev Rupert.SO3 line 75 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Submonoid, Matrix, Fin, OfNat.ofNat, Nat, Real
Proof uses: Matrix.specialOrthogonalGroup
13 instances, coercions and auxiliary constants left out.
def Rupert.transformed_shadow The result of transforming a subset of ℝ³ by a chosen rotation and offset, and then projected to ℝ² line 84 source
Source documentation
The result of transforming a subset of ℝ³ by a chosen rotation and offset, and then projected to ℝ².

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Fin, OfNat.ofNat, Nat, Real, Subtype, Matrix, Membership.mem, Submonoid, Rupert.SO3
Proof uses: Set.image, HAdd.hAdd, Function.comp, Matrix.mulVec, Fin.castSucc
31 instances, coercions and auxiliary constants left out.
```
def transformed_shadow (X : Set ℝ³) (offset : ℝ²) (rotation : SO3) : Set ℝ² :=
…
```
Mentions: Rupert.SO3
def Rupert.IsRupert Documented declaration: IsRupert line 103 source
Source documentation
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.]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Fin, OfNat.ofNat, Nat, Real
Proof uses: Exists, Subtype, Matrix, Membership.mem, Submonoid, Rupert.SO3, Set, Rupert.transformed_shadow, ClosureOperator, convexHull, LE.le, interior
36 instances, coercions and auxiliary constants left out.
```
def IsRupert (vertices : Finset ℝ³) : Prop :=
…
```
theorem Rupert.is_every_convex_polyhedron_rupert There exists a convex polyhedron with nonempty interior for which the Rupert property does not hold sorry line 114 source
Source documentation
There exists a convex polyhedron with nonempty interior for which the Rupert property does not hold.

depends on sorry what this means
Statement uses: Iff, False, Finset, Fin, OfNat.ofNat, Nat, Real, Set.Nonempty, interior, ClosureOperator, Set, convexHull, Rupert.IsRupert
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem is_every_convex_polyhedron_rupert :
    answer(False) ↔ ∀ (vertices : Finset ℝ³),
       (interior (convexHull ℝ vertices : Set ℝ³)).Nonempty → IsRupert vertices := by
…
```
Mentions: Rupert.IsRupert