Rupert.lean

Stream: general

[David Renshaw]

With help from @Jason Reed, I have been formalizing the Rupert Property for various convex polyhedra: https://github.com/dwrensha/Rupert.lean

Today I released a video explaining my proof for the triakis tetrahedron, which is one where there is only a very slim margin: https://youtu.be/jDTPBdxmxKw

[Bolton Bailey]

As I recall, your original video mentioned a number of polyhedra for which the Rupert Property status was open. Now that you have formalized the Rupert property, might this make a good inclusion into the formal-conjectures repository?

[David Renshaw]

Yes, I think that's a good idea.

[Jason Reed]

Bolton Bailey said:

As I recall, your original video mentioned a number of polyhedra for which the Rupert Property status was open. Now that you have formalized the Rupert property, might this make a good inclusion into the formal-conjectures repository?

I think I'm going to try to take a crack at this. @David Renshaw suggested to me we might want to rework the definition of Rupertness a little bit to not depend on the definitional equality of EuclideanSpace and Fin n -> R , because it seems that's going to go away eventually.

[Jason Reed]

I filed https://github.com/google-deepmind/formal-conjectures/issues/283

[David Renshaw]

The conjecture I put more faith in is "there exists a convex polyhedron that does not have the Rupert property" (the negation of what you propose).

[Jason Reed]

I agree that that's where my sympathies lie as well. I'm currently looking through the formal-conjectures style guide and it appears there is a way of stating things that presumes more neutrality.

[Jason Reed]

Point 6 in https://github.com/google-deepmind/formal-conjectures?tab=readme-ov-file#style-guidelines

[Jason Reed]

I was initially biased towards formalizing the "every convex polyhedron is Rupert" formulation because the earliest available citation phrased it that way

With a certain hesitancy, we even suggest that perhaps every
convex polyhedron in R3 has the Rupert property

[Jason Reed]

albeit "with a certain hesitancy" :slight_smile:

[Kevin Buzzard]

The sphere does not, so one might imagine that all "sufficiently round" convex polyhedra fail too. The rhombicosidodecahedron is an archimedean solid which I'm particularly fond of because it's the physically largest Archimedean solid which I can make with my polydron collection; I was not surprised to see it on the unknown list when I discovered today that there were some unknown examples and it wouldn't surprise me if this were not Rupert.

[Jason Reed]

Do you have any sense for what notions of "sufficiently spherical" might be workable? I understand that's a pretty far out speculative thing to ask, but maybe you have more discrete geometry intuition than I do...

[Kevin Buzzard]

I meant "the biggest possible Archimedean solid I can make with my polydron" which can probably translated into some assertion about curvature or something. The angle at a vertex is 108+90+60+90 which is only 12 degrees off 360.

[Jason Reed]

Yeah, "angle deficit" is an example for what I was fishing for, I guess: i.e. what metrics of sphericality might be most relevant. One could also imagine, I don't know, ratio of outer to inner diameter or something.

in any case I definitely agree on an intuitive level that roundness/sphericality feels like the essential obstacle to Rupertness.

[Kevin Buzzard]

I am surprised that this question is open. It seems to me like it's just a messy but finite calculation (because SO(3) is compact).

[Jason Reed]

I am currently working on whipping up some rust code to try to do that by brute force

[Jason Reed]

I tried throwing it over the wall to real-closed-field solvers but they either segfaulted (QEPCAD) or ran longer than my patience (redlog)

[Junyan Xu]

Is the two-dimensional case too trivial that I can't find any reference? I can see that the equilateral triangle is Rupert while the square is not.

[Jason Reed]

@Sean McLaughlin iirc suggested that "7 variables to be quantifier-eliminated and degree-6 polynomials" is in fact decently deep into the double-exponential territory to be not surprising that it gets hard

[Jason Reed]

@Junyan Xu why is the square not rupert in 2d? I'd reckon it is, but maybe you're thinking about it differently

[Junyan Xu]

I think it boils down to a+b>c=sqrt(a^2+b^2) if a,b>0 (c is the side length)

[Junyan Xu]

BTW whether a polyhedron is Rupert is decidable, but the algorithm isn't efficient enough: user_uploads/thumbnail/3121/pP06hILgzy-Oh-0rAnafYRkf/image.png/840x560.webp

[Jason Reed]

I agree it's decidable, because the theory of real closed fields is decidable

[Junyan Xu]

Oh sorry, the square is indeed Rupert

[Jason Reed]

When I say "the square is rupert in R^2" I mean
image.png

[Jason Reed]

There exists two SE(2) such that upon projection to R^1, the shadow of one transformed square is inside the shadow of the other

[Jason Reed]

I wouldn't find it unreasonable if someone thought this didn't count because, like, the square gets split into two pieces... but I imagine the triangle wouldn't be rupert either on that definition

[Jason Reed]

$S^0$ being disconnected is exceptional :slight_smile:

[Jason Reed]

But um... I think I might go out on a limb and guess that every convex polygon is Rupert

[Jason Reed]

You can't make a https://en.wikipedia.org/wiki/Curve_of_constant_width with only finitely many sides, can you?

[Junyan Xu]

Yeah, it's claimed here on Wikipedia: "no polygon can have constant width". I think that solves it. Thanks!

[Junyan Xu]

Some more recent work on computation include
Optimizing for the Rupert property (where my screenshot above is taken from; it's published but I don't have access) (GitHub repo)
Some upsetting things about shapes that we already knew (found through David's earlier video)

[Jason Reed]

Oh yeah, I'll make sure to cite that as well, thanks!

[Jason Reed]

Submitted https://github.com/google-deepmind/formal-conjectures/pull/284

[Joseph Myers]

Jason Reed said:

I think I'm going to try to take a crack at this. David Renshaw suggested to me we might want to rework the definition of Rupertness a little bit to not depend on the definitional equality of EuclideanSpace and Fin n -> R , because it seems that's going to go away eventually.

We should have everything in mathlib needed to make a definition in proper mathlib generality. Work in an affine space over a finite-dimensional real inner product space, rather than talking about specialOrthogonalGroup consider all AffineIsometry whose underlying linear map has positive determinant (we already have the lemma that this is equivalent to being orientation-preserving), and the projections are EuclideanGeometry.orthogonalProjection onto an affine subspace satisfying IsCoatom (which such subspace you choose obviously doesn't actually matter since there are orientation-preserving isometries mapping any coatom subspace to any other, although you might need to fill out some API to prove that).

[Joseph Myers]

Is it out of scope for this repository to justify that the coordinates you're using for the vertices of certain polyhedra do in fact yield the desired polyhedron as determined by its more abstract mathematical properties?

[David Renshaw]

Can you give an example of how you'd define a polyhedron more abstractly?

[Jason Reed]

We should have everything in mathlib needed to make a definition in proper mathlib generality...

Huh, I hadn't considered generalizing beyond R^3, but I think everything you're saying here seems sensible. Higher-dimensional variants have been studied at least. I don't know if other base inner product spaces besides R have been.

[Jason Reed]

Do you think a suitably general IsRupert ought to be in mathlib? That would make the formal-conjectures PR tidier. I'm happy to investigate that a bit if so. (but your pointers as to what concerns are likely to come up are very helpful)

[Joseph Myers]

Maybe you need to work around the convexity refactor not having been done yet and so convexHull not being defined for affine spaces. Or simply define for an inner product space rather than an affine space over it and leave the affine refactoring for after the convexity refactor.

(Once you're proving things for a concrete choice of polyhedron, using EuclideanSpace makes sense. The fact that any DilationEquiv between different spaces preserves this property, so that the result for "this choice of triakis tetrahedron" is equivalent to the one for "a triakis tetrahedron of any scale and orientation and position in any 3-dimensional Euclidean space", should be a routine lemma.)

[Joseph Myers]

I think putting the definition in mathlib makes sense, yes. After all, it will be used by both your repository and formal-conjectures, and formal-conjectures probably doesn't want to depend on lots of other repositories each with a few definitions.

While I think defining the Archimedean and Catalan solids would be reasonable for mathlib as well, that seems like a larger project, since it engages the tricky question of what concept of "polyhedron" to define, and mathlib probably shouldn't have definitions just by giving coordinates without also proving they satisfy some characteristic property (e.g. convex, vertex-transitive and a given sequence of regular polygons at each vertex, for Archimedean polyhedra, with the Catalan solids then being derived from the Archimedean ones by pole-polar reciprocation).

[Mario Carneiro]

The presentation in your video @David Renshaw and also Tom7's paper assume that rupertness only needs you to consider a straight line path. But is it known whether this is equivalent to any path, or maybe there is some couch-problem-type solution where giving it a little wiggle in the middle of the path helps it make it through?

[Jason Reed]

@Mario Carneiro I also wondered this when I was first exposed to Rupert stuff (and I saw the same question asked here a few years back) but I don't know if that extra generality ever helps you or if anyone's seriously studied it

[Joseph Myers]

On further consideration, I think you can avoid the convexity refactor issue (and write a definition that applies in affine spaces) by defining IsRupert as a property on sets of points that's only mathematically meaningful when those are convex, so passing the convex hull into IsRupert rather than passing in an indexed family of vertices and having it apply convexHull itself.

The statement proposed for formal-conjectures is described as "Does the Rupert property hold of every convex polyhedron with nonempty interior?" but it looks like the actual formal statement uses "nonempty convex hull" not "nonempty interior", so I'd expect it to be boringly false for a family with a single point.

[Jason Reed]

Oops, that's definitely an unintentional omission. (of "interior" in the PR) Thanks for catching that.

About generalizing to arbitrary sets, I'm inclined to agree with you. I did introduce a non-polyhedron-specific definition of IsRupertSet in https://github.com/dwrensha/Rupert.lean/blob/main/Rupert/Set.lean but I think a combination of @David Renshaw persuading me it was clearer and/or trying to be closer to the literature convinced me at the time that the polyhedral definition was better to highlight as the "main" one, and then subsequently I proved that the two definitions coincided under the appropriate assumptions.

So I'm all for "mathlib has a definition of IsRupert that says of a subset of an arbitrary affine space that it admits two affine isometries that appropriately project to a codimension-1 subspace, etc. etc." and "formal-conjectures poses the question of whether arbitrary finite subsets of R^3 (or perhaps even R^n?) with nonempty convex hull interior satisfy that property"

I think in fact it is perfectly meaningful to ask the question of whether a nonconvex set is Rupert; although it might have less tight of a connection to the original intuition of "cutting a single hole in an object", since now the resulting topology might be more complicated.

[Jason Reed]

I think my plan is to start from

import Mathlib

def GeneralizedIsRupert {P : Type*} [MetricSpace P] [NormedAddTorsor ℝ P]
    (X : Set P) : Prop :=
    ∃ (inner_isometry outer_isometry : AffineIsometry ℝ P P)
      (Q : AffineSubspace ℝ P) (_ : Nonempty Q) (_ : IsCoatom Q),
    let proj := EuclideanGeometry.orthogonalProjection Q
    closure ((proj ∘ inner_isometry) '' X) ⊆ interior ((proj ∘ outer_isometry) '' X)

and try to prove that this coincides with the IsRupertSet that we have in our little repo.

Does anything jump out at you, @Joseph Myers, as not representing what you had in mind? I tried to make the typeclass assumptions on P as minimal as possible guided by what error messages came out of various things requiring them. But I'm not sure I did an optimal job considering the complexity of definitions in mathlib...

[Jason Reed]

(Oh, and as an aside I don't think the motivation of the closure here (and also occurring here) was previously discussed in this thread, but it's something that appeared during @David Renshaw and my conversations earlier elsewhere... to say clo X subset int Y seems like a nice purely topological way of saying "X fits well within Y", which accords with our intuition that both the open and closed balls should not be Rupert. For the case of polyhedra defined as the convex combination of a finite set it's moot, since they're compact by construction)

[Joseph Myers]

That definition says P is a one-dimensional space (a torsor for the reals themselves), you need to have a real inner product space V for which P is a torsor. It's also missing the positive determinant (orientation preserving) part - when discussing the open problem of whether the snub cube is Rupert, people definitely seem to expect that it can only be rotated, that you can't reflect one snub cube before trying to pass it through another.

[Jason Reed]

Ah, that would certainly explain why I was failing to find an instance for R^n :man_facepalming:.

As for reflection, I believe it leads to an equivalent definition whether it's allowed or not: since we're projecting down to a smaller subspace anyhow, if we could find an affine isometry f that mapped a set X to a desirable image (proj ∘ f) '' X but had determinant -1, we could compose with a reflection about the subspace proj is projecting onto (i.e. λy. 2 proj y - y) and find that (λy. 2 proj y - y) ∘ f is the desired orientation-preserving isometry with the same effect on X:
(proj ∘ (λy. 2 proj y - y) ∘ f) '' X = ((λy. 2 proj y - proj y) ∘ f) '' X = (proj ∘ f) '' X
Or am I missing something? Or assuming more structure than I'm licensed to in this general setting? I'm afraid I might be...

[Mario Carneiro]

I agree, the projection should come out the same whether you are allowed to reverse orientation or not

[Mario Carneiro]

at least in R^n

[Joseph Myers]

Yes, that seems sound as a reason why you don't need the orientation-preserving condition. You can put a formal proof of something like that when proving equivalence to the definition you had using specialOrthogonalGroup.

[Jason Reed]

Good, exactly, that's what I was imagining doing

[Joseph Myers]

One thing to consider for definitions is whether to include a definition of the Nieuwland number somewhere (so the Rupert property is equivalent to that being greater than 1).

[Mario Carneiro]

Any idea how one might state couch-problem-rupert where you are allowed to move the inner shape continuously along a path? And prove that it has the obvious relation with the normal rupert property?

[Jason Reed]

Yeah I thought I was achieving something like a genuinely more general topological analogue of Nieuwland > 1 by saying closure X sub interior Y

[Jason Reed]

but I still need a norm around for the notion of isometry

[Jason Reed]

So I suppose Nieuwland > 1 <=> Rupert-as-i've-proposed-here is still a thing that could be stated and proven potentially

[Jason Reed]

Mario Carneiro said:

Any idea how one might state couch-problem-rupert where you are allowed to move the inner shape continuously along a path? And prove that it has the obvious relation with the normal rupert property?

The difficulty with this for me is I don't have a guess for how to formalize what it means to "cut a hole through a shape" other than the straight-line non-couch projection

[Mario Carneiro]

the hard part seems to be determining what constitutes a valid cutting. Maybe something like the left behind object has the homotopy type of a circle

[Mario Carneiro]

but I think that doesn't work because you can go halfway in, poke a tiny hole in the back end, then come back out

[Jason Reed]

Yeah that occurred to me... in that case I think you'd want to actually exhibit a full path of the "cutting" copy that in some sense belongs to the homotopy class of 1 \in Z

[Mario Carneiro]

something something knot theory

[Jason Reed]

I mean this definitely feels very homotopy-ish

[Joseph Myers]

Continuous path = real-indexed sequence of isometric copies continuous with respect to Hausdorff distance, I suppose, so the problem of what counts as passing through another copy of the set is indeed the hard part.

[Mario Carneiro]

is SO(n) known to be a a topological manifold?

[Jason Reed]

surely

[Jason Reed]

differentiable manifold as well, no?

[Jason Reed]

lie groups and lie algebras and all

[Joseph Myers]

But we might not have the topology on it in mathlib.

[Mario Carneiro]

or maybe the space of isometries is more relevant

[Mario Carneiro]

if you make the motion a closed loop, then I think you can say that the center traces a path which is not null-homotopic in the complement of the cutout shape

[Jason Reed]

Yes, that's what I meant by 1 \in Z

[Jason Reed]

the homotopy group of the complement of the circle is Z, and the path should be one full loop through it

[Jason Reed]

at least I'd think so? I'm not sure what it would mean if you needed, like 2 loops through or something

[Mario Carneiro]

not null-homotopic allows all of those

[Jason Reed]

true

[Jason Reed]

maybe that's a cleaner definition then

[Mario Carneiro]

same if the cutout shape isn't homotopically a circle

[Mario Carneiro]

which I think could happen with some motions

[Jason Reed]

What if the candidate shape for rupertness is already not contractible

[Jason Reed]

Is (and I never thought I'd be saying this sentence) the donut couch-Rupert?

[Mario Carneiro]

it's probably not hard to adjust the cube in cube motion to nick the side as it goes through and make a double torus

[Mario Carneiro]

it could do a bit of carving work before the main path too

[Mario Carneiro]

I believe the torus is not rupert, because no matter how you turn it always has two extremal points which are the major diameter apart. The line segment between these two points will have to coincide with the analogous line segment for the outer torus at some point in the motion

[Mario Carneiro]

the same argument should apply to anything like an oblate spheroid which has a circle of extremal points larger than the rest of the shape

[Jason Reed]

I think it's possible to carve some little tube of a hole through the cube such that the usual rotation-pair witness that the cube is rupert still works for projective-Rupertness

[Jason Reed]

but is that valid for couch-Rupertness if the cutting passes through the hole? Should it be that the the homotopy type is altered appropriately to reflect one more hole being added?

[Mario Carneiro]

in my definition it would still count

[Jason Reed]

@Joseph Myers , I appreciate your patience helping me with this; another question. Should I expect an instance of Q.direction.HasOrthogonalProjection to be inferred, in the following #mwe-able self-contained example?

import Mathlib

def IsAffineRupertPair {P : Type*} {V : Type*} [MetricSpace P] [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    [NormedAddTorsor V P]
    (inner outer : Set P) : Prop :=
    ∃ (inner_isometry outer_isometry : AffineIsometry ℝ P P)
      (Q : AffineSubspace ℝ P) (_ : Nonempty Q)
      (_ : Q.direction.HasOrthogonalProjection) -- should I need this?
      (_ : IsCoatom Q),
    let proj := EuclideanGeometry.orthogonalProjection Q
    let inner_shadow := (proj ∘ inner_isometry) '' inner
    let outer_shadow: Set Q := (proj ∘ outer_isometry) '' outer
    closure inner_shadow ⊆ interior outer_shadow

I thought I didn't, but I get a heartbeat timeout if I remove it.

[Mario Carneiro]

maybe a better example for what you are going for is a square hoop; this is couch-rupert by my definition and you don't even need to cut out material to do so, but it's not rupert because it's passing through an area which is not covered by the original shape

[Jason Reed]

That is an interesting example. Something about it makes my intuition want to protest that it's not rupert, because there's no cutting! Clearly that's cheating :)

[Jason Reed]

(although I'm just saying this in jest, I don't really have a strong commitment to one definition or other...)

[Mario Carneiro]

I would like rupert to imply couch-rupert, but I don't know whether that needs a modification to the definition or whether it is just only true for convex bodies

[Jason Reed]

Yeah, I agree rupert implies couch-rupert seems desirable. Couch-rupertness for disconnected subsets also starts straining my intuition. Is A couch-rupert with respect to B?
image.png

[Jason Reed]

I can pass A through B leaving two holes...

[Mario Carneiro]

My definition also talks about the "center" making a path, but what if the center isn't in shape A at all?

[Jason Reed]

Yeah, that's what I was thinking of, in part.

[Jason Reed]

Counting how many holes are created and controlling in what sense they're homotopically passed through seems very messy.

[Joseph Myers]

You get to set up the API for atoms and coatoms in affine spaces. We have no such API at all at present. (And once you've shown that a coatom has a coatom direction, you then need to show that a coatom has orthogonal projections in an inner product space. I'm not actually sure if that's true in general for cases such as infinite-dimensional spaces that aren't complete, or if we need additional conditions to ensure coatoms have orthogonal projections.)

[Jason Reed]

And yet this pair is definitely projectively rupert.

[Mario Carneiro]

I wonder if there is a sense that the whole motion is knotted inside a higher dimensional space?

[Mario Carneiro]

We have a space of isometries, and the motion in question stays clear of the cutout shape by definition. So this is a path in the space which stays within the set of isometries that do not touch the cutout shape, and that path is not null homotopic

[Jason Reed]

Joseph Myers said:

You get to set up the API for atoms and coatoms in affine spaces. ...

Ok, great, that is a solid "no, I shouldn't expect this to work yet" answer, thanks :)
I'll try to dig in and try to understand the actual library code some more then...

[Jason Reed]

@Joseph Myers actually, it turns out assuming [FiniteDimensional ℝ V] suffices for an instance of Q.direction.HasOrthogonalProjection to be inferred. I presume though I haven't checked that the dominoes involved in the chain are that V's finiteness entails P's given [NormedAddTorsor V P], and then Q as a subspace of P is also surely finite, and then Q.direction is finite because Q is. Hence Q.direction admits orthogonal projections.

Assuming completeness of V doesn't seem to automatically transfer to the completeness of Q.direction. I don't know if this is because it's actually false, or merely because the appropriate instance declarations don't exist yet. Nonetheless, infinite-dimensional linear algebra is beyond the frontier of my mathematical confidence, and I'd be happy restricting attention to the finite dimensional case, if you don't think that's too big a generality penalty?

[Jason Reed]

My current code is a PR against dwrensha/Rupert.lean, I'm intending to work on it a bit there and at some future point try to upstream it to mathlib

[Jason Reed]

I assume fleshing out the API for coatoms will still be needed for the proof of equivalence of definitions

[Joseph Myers]

Assuming FiniteDimensional seems reasonable for now.

[Kenny Lau]

you know, this reminds me of a very old meme

[Kenny Lau]

the one where everything fits in the square hole

[Yaël Dillies]

Here's a preprint claiming to construct a non-Rupert polyhedron: https://arxiv.org/abs/2508.18475

[Jason Reed]

Oh! Very interesting, I'll have to check it out.

[Jason Reed]

So far from a quick skim it looks like it makes sense to me, and follows a very similar approach to what my collaborators and I were taking. Seems like they had some cleverness in choosing a good polyhedron that let them cut down from 7 dimensions of search space to 5. Their "rigorous[] [confirmation] that [their theorems] indeed apply for all 18 million regions and that indeed the union of the regions covers the initial search space" is a matter of running some sagemath code, though, so that admits the possibility of improvement.

[Jason Reed]

The repository https://www.github.com/Jakob256/Rupert said to contain the sage code is not accessible; perhaps they're waiting for publication (of the paper) to publicize it

[David Renshaw]

The repo appears to be public now. https://www.github.com/Jakob256/Rupert

[David Renshaw]

@Jason Reed and I have begun working on a formalization of the Noperthedron proof: https://jcreedcmu.github.io/Noperthedron/

We've already put in place a basic skeleton of the argument, as can be seen in our dependency graph. The exists_solution_table node corresponds to the big computational verification of 18 million regions. We think we can do that in Lean (possibly requiring the native compiler). Our first target, however, will be to formalize the rest of the math, of which there is a fair amount!

We have plenty of proofs to write, so we welcome any help. There are some juicy sorries about trig function approximations, partial derivatives, and inequalities involving norms and inner products in Euclidean spaces.

[David Renshaw]

We have been made aware that @ohhaimark has been making a parallel effort on the same problem: https://github.com/badly-drawn-wizards/noperthedron .
Fortunately, it looks like there has not been a lot of duplicated work between the two repositories.

[Jason Reed]

Would be great to combine results!

[ohhaimark]

Heyo. I'm looking at the blueprint. The last point I left my repo there was hairy dependency on Schur decomposition . It is not yet in Mathlib, but was in a PR limbo. Namely lemma 12 of the paper invokes a matrix form of Euler's rotation theorem. Following Wikipedia's approach would require use of Schur decomposition. I am no expert, so maybe there is an easy sidestep of the whole thing.

[Jason Reed]

Interesting! Fwiw, I'd be comfortable leaving that dependency as a sorry for now. Not seeing a shortcut to "every rotation matrix is conjugate to an x-axis rotation" yet, but maybe there is one...

[Jason Reed]

I did have a definition in an older repo that could locate the rotation that took a given vector to another, (i.e. the second step of "(1) every rotation is a rotation about an axis, (2) rotate that axis to align with the x axis") but with quaternionic rotations, and... I see also the proof that it worked was not completed.