8 Computational Step
We define rational approximations of the 90 noperthedron vertices by \(\lfloor x \cdot 10^{16} \rfloor /10^{16}\).
nopertQ is a \(\kappa \)-rational approximation of the Noperthedron.
There exists a valid solution table whose zeroth row covers
By exhibiting the table and running the validity checking algorithm. Formalized as Noperthedron.NativeCaseAnalysis.solutionTable in the build-on-demand NativeCaseAnalysis library (checked with native_decide) and independently in the kernel-only KernelCaseAnalysis library (checked with decide +kernel, using only the standard axioms); both are kept out of the default build targets so that CI runs stay fast.
If a global node in the solution tree is valid, then there is no Rupert solution for its interval.
If a local node in the solution tree is valid, then there is no Rupert solution for its interval.
If we have a valid solution table, and in particular its \(i\)th row is valid, then there is no Rupert solution of the interval of its \(i\)th row.
By strong induction on the number of rows left in the table following the \(i\)th. This is because validity constrains each row to only refer to later entries. For a split row, every point in its interval belongs to a child interval at a larger index, so the induction hypothesis excludes a Rupert solution there. At a leaf, apply Theorem 54 or Theorem 55.
If we have a valid solution table, then there is no Rupert solution of the interval of its zeroth row.
Immediate special case of theorem 56.