9 The case analysis and the main theorem
9.1 Root boxes
There are 15 root boxes, all with \((u, v) \in [0, 1] \times [0, \frac12]\):
charts \(1, 2, 3\) with \(r \in [-1, 1]^3\);
chart \(0\), one box for each face \(f\), with \((s_0, s_1) \in [-1,1]^2\) and \(\rho \in [0, 1]\);
chart \(4\), one box for each face \(f\), with \((s_0, s_1) \in [-1,1]^2\) and \(\rho \in [0, 2]\).
Every reduced \((u, v, j, r)\) is a point of one of the root boxes of chart \(j\).
The wedge and disk conditions give \(0 \le u \le 1\) and \(0 \le v \le \frac{57}{128}u \le \frac12\). In charts 1–3, \(|r_i| \le 1\). In charts 0 and 4, Lemma 37 writes \(r = \rho \, c_f(s_0, s_1)\) with \(0 \le \rho \le 1\) or \(0 \le \rho \le 2\).
9.2 The tree walk
A certificate tree has internal nodes that split a box in half along one coordinate, and leaves that are gap leaves or domain leaves. A tree is accepted on a box if every leaf passes on its sub-box.
Splitting halves one radius \(h_i\); if \(h_i\) is odd, the scale \(K\) is first increased by one and all centres and radii are doubled, so that box coordinates stay integers.
Every point of a box is a point of one of its two halves.
If \(t_d \le 0\) the point is the point of the lower half at \(2 t_d + 1\), otherwise of the upper half at \(2 t_d - 1\).
If a tree is accepted on a box, then the box is covered.
For the kernel check the tree of each root box is cut into a skeleton whose leaves include holes, and a list of subtrees, one for each hole, each checked by a separate theorem.
If the skeleton is accepted on a root box when holes count as passing, its holes are exactly the boxes of the listed subtrees, and every listed subtree is accepted on its box, then the root box is covered.
A bad point of the root box lies in a hole, by the same induction as Theorem 66, and the hole’s box is covered.
9.3 The main theorem
If each of the 15 root boxes carries an accepted skeleton with accepted subtrees for its holes, then \(\operatorname{\mathbf{P}}\) is not Rupert.
The certificate has \(245{,}484\) leaves. It is generated by a floating-point search (cayley/search) and cut into \(28{,}082\) chunks of at most 16 leaves. For each chunk, the statement that the checker accepts it is proved by Eq.refl true, so the Lean kernel evaluates the checker on that chunk. The kernel-checked theorems live in CayleyKernel/Main.lean; they are not part of the default build, since they need the generated data.
The Noperthedron is not Rupert (Cayley.KProof.noperthedron_not_rupert). Hence there is a convex polyhedron with nonempty interior that is not Rupert (Cayley.KProof.exists_not_rupert).