8 Computational Step

Theorem 60

There exists a valid solution table whose zeroth row covers

\begin{align*} \theta _1,\theta _2& \in [0,2\pi /15] \subset [0,0.42], \\ \varphi _1& \in [0,\pi ] \subset [0,3.15],\\ \varphi _2& \in [0,\pi /2] \subset [0,1.58],\\ \alpha & \in [-\pi /2,\pi /2] \subset [-1.58,1.58]. \end{align*}

Proof ▶

By exhibiting the table and running the validity checking algorithm.

Theorem 61

If a global node in the solution tree is valid, then there is no Rupert solution for its interval.

Proof ▶

Theorem 62

If a local node in the solution tree is valid, then there is no Rupert solution for its interval.

Proof ▶

Theorem 63

✓

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.

Proof ▶

By a mutual 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. Appeal inductively to this same theorem if the row splits into other nodes in the tree, or appeal to Theorem 61 or Theorem 62) at the leaves.

Corollary 64

✓

If we have a valid solution table, then there is no Rupert solution of the interval of its zeroth row.

Proof ▶

Immediate special case of theorem 63.