1 Introduction

Steininger and Yurkevich [ SY25 ] constructed a convex polyhedron, the Noperthedron, and proved that it does not have Rupert’s property: no copy of it can be passed through a hole in another copy. This blueprint describes a Lean proof of the same theorem that is checked by the Lean kernel alone, using only the standard axioms.

The overall strategy agrees with [ SY25 ] : reduce to purely rotational passages, use the symmetries of the Noperthedron to shrink the space of rotation pairs to a bounded box, cover that box by a large tree of sub-boxes, and exclude each sub-box by exhibiting an inner vertex whose shadow lies outside the outer shadow. The details differ in several ways.

Rational coordinates. Rotations are parametrized by Cayley coordinates (Chapter 4) instead of angles. Every rotation matrix in the case analysis is a rational function of the box coordinates, so every leaf check is exact polynomial arithmetic. The only irrational numbers are the fixed constants \(\cos (2\pi k/15)\), \(\sin (2\pi k/15)\) and the vertices (Chapter 8).
A different reduction. The symmetry reduction (Chapter 5) puts the outer view in a wedge, picks the relative rotation from its orbit under the symmetries by maximizing a score, and covers the result by five Cayley charts.
No local theorem. Near the configurations where the inner and outer shadows coincide, [ SY25 ] uses a separate local argument. Here these configurations are blown up (Section 6.3): the vanishing gap factors exactly, and the remaining factor is checked like any other polynomial.
Polynomial bounds instead of Lipschitz bounds. A box is excluded by a lower bound of a polynomial on \([-1,1]^5\) (Chapter 7), computed from its coefficients or from its Bernstein coefficients.

The case analysis is a tree with \(245{,}484\) leaves. It is produced by an untrusted floating-point search and checked by a Lean function that the kernel evaluates (Chapter 9).