6 Boxes and leaf certificates
6.1 Boxes
A box consists of a chart \(j \in \{ 0, \dots , 4\} \), a face \(f \in \{ 0, \dots , 5\} \) (used only in charts 0 and 4), a scale \(K \in \operatorname{\mathbb {N}}\), and integer centres \(c_i\) and radii \(h_i \ge 0\) for \(i = 0, \dots , 4\). The point of the box at normalized coordinates \(t \in [-1,1]^5\) is \(X(t)\) with \(X_i = (c_i + h_i t_i) / 2^K\).
Normalizing every box to \([-1,1]^5\) means that every polynomial below is bounded on the same cube.
A point \(X\) of a box is bad if, with \(r\) the Cayley vector of \(X\) (Definition 36), the tuple \((X_0, X_1, j, r)\) is reduced and \(\bigl(s(X_0, X_1),\ s(X_0, X_1)\, Q_j(r)\bigr)\) is a Rupert pair. A box is covered if none of its points with \(X_0^2 + X_1^2 \le 1\) and \(|r_i| \le 2\) is bad.
The certificate is a binary tree for each root box. Each internal node halves the box along one coordinate; each leaf is either a gap leaf, which shows that no point of the box gives a Rupert pair, or a domain leaf, which shows that no point of the box is reduced.
6.2 The gap polynomial
Fix a box in chart \(j\), an inner vertex \(S\), an outer vertex \(T\) and a direction \(w \in \operatorname{\mathbb {Z}}^2 \setminus \{ 0\} \). The separation criterion (Theorem 13) asks for
Multiplying by the positive denominators \(D_o = 1 + u^2 + v^2\) and \(D_r = D(r)\) and by an integer \(\kappa _j \ge 1\) that makes \(M_j = \kappa _j B_j\) an integer matrix (\(\kappa _j = 1\) for \(j \le 3\), and \(\kappa _4 = x^2 + y^2\) in the notation of Definition 27, after scaling \(C_3\) to integers) clears every denominator.
where \(N_o\) is the numerator of \(s(u, v)\). As a function of the normalized coordinates \(t\), this is (up to a fixed power of two) a polynomial with integer coefficients of degree at most \(2\) in each variable. Writing \(\alpha _k = w_0 (N_o)_{0k} + w_1 (N_o)_{1k}\), it equals \(A - \sum _k T_k E_k\) with \(A = \sum _k \alpha _k (M_j N(r) S)_k\) and \(E_k = \alpha _k \kappa _j D_r\), which do not depend on \(T\).
\(D_o\, s = N_o\) and \(D_r \mathrm{Cay}(r) = N(r)\); the entries of \(N_o\) have degree at most \(2\) in each of \(u, v\), and the entries of \(N(r)\) and \(D_r\) have degree at most \(2\) in each of \(r_0, r_1, r_2\) (or of \(s_0, s_1, \rho \) in the blown-up charts, where \(r = \rho \, c_f(s_0, s_1)\)). The product is bilinear in these two groups of variables.
The checker uses dyadic approximations \(\hat S\), \(\hat T\) of the vertices with error at most \(2^{-60}\) per coordinate (Lemma 60). The error is absorbed by an explicit allowance \(\mathrm{err} = 128\, \kappa _j\, 2^{-60} (|w_0| + |w_1|)\); this uses \(u^2 + v^2 \le 1\), \(|r_i| \le 2\) and the fact that orthogonal matrices do not enlarge vectors.
6.3 The blow-up
In charts 0 and 4 each inner vertex \(S\) has a paired outer vertex \(\sigma (S)\): \(\sigma (S) = S\) in chart 0, and in chart 4 \(\sigma (S) = \tau S\) for the 30 copies of \(C_3\) (Lemma 28). At \(r = 0\) the pair has \(Q_j(0) S = B_j S = \sigma (S)\), so \(\mathrm{gap}_{\sigma (S)}\) vanishes identically on \(\rho = 0\), and no box touching \(\rho = 0\) can have a positive lower bound for it.
In charts 0 and 4, with \(r = \rho \, c\),
\(Q_j(r) S - \sigma (S) = B_j(\mathrm{Cay}(r) S - S)\) in both charts (for chart 4, \(\sigma (S) = \tau S = B_4 S\)). Apply Lemma 16 and \(r = \rho c\).
The bracket \(L\) is again a polynomial of degree at most \(2\) in each variable. It does not vanish at \(\rho = 0\), so it can be bounded below on boxes that touch \(\rho = 0\). Since \(\rho \ge 0\), \(L \ge 0\) implies \(\mathrm{gap}_{\sigma (S)} \ge 0\).
Let \(X\) be a point of a box in chart \(j\) with \(u^2 + v^2 \le 1\) and \(|r_i| \le 2\), let \(S\) be an inner vertex and \(w \ne 0\). Suppose that for every outer vertex \(T\), either
or \(j \in \{ 0, 4\} \), \(T = \sigma (S)\) and \(\mathrm{err} \le 2 \hat L(X)\), where \(\hat L\) is \(L\) computed with \(\hat S\). Then \(\bigl(s, s\, Q_j(r)\bigr)\) is not a Rupert pair.
In both cases the true gap \(\mathrm{gap}_T(X)\) is nonnegative once the approximation error is accounted for, so the separation criterion (Theorem 13) applies with the inner vertex \(S\) and direction \(w\).
6.4 Gap leaves
A gap leaf names an inner vertex \(S\) and a direction \((w_0, w_1) \ne 0\). It passes if the coefficients of the polynomials involved are small enough for the packed arithmetic of Chapter 7, and for every one of the 90 outer vertices \(T\) one of the following succeeds:
the quick test: a lower bound of \(A - \sum _k T_k E_k\) built from the constant terms and coefficient sums of \(A\) and the \(E_k\), evaluated for all 90 vertices at once;
the full test: the coefficient lower bound or the Bernstein lower bound of the polynomial \(A - \sum _k \hat T_k E_k\) is at least \(\mathrm{err}\);
for the paired vertex \(T = \sigma (S)\) in charts 0 and 4: the coefficient or Bernstein lower bound of \(2L\) is at least \(\mathrm{err}\) (or \(\rho {\gt} 0\) on the whole box and the full test succeeds).
If a gap leaf passes on a box, then no point of the box with \(u^2 + v^2 \le 1\) and \(|r_i| \le 2\) gives a Rupert pair \((s, s\, Q_j(r))\).
Suppose \(A \ge c_0 - \mathrm{sl}\) and \(|E_k - e_k| \le a_k\) on the box, where \(c_0\), \(e_k\) are constant terms and \(\mathrm{sl}\), \(a_k\) are coefficient sums. If
then \(\mathrm{err} \le A - \sum _k T_k E_k\) on the box.
Linear arithmetic.
6.5 Domain leaves
A domain leaf names one condition of Definition 34 that fails on the whole box:
(disk) \(u^2 + v^2 {\gt} 1\), tested at the lower corner of the box;
(wedge) \(v {\gt} \frac{57}{128} u\), tested at the corners of the box;
(chart \(k\)) \(\operatorname{\mathrm{tr}}(B_j^T Q_j(r)) {\lt} \operatorname{\mathrm{tr}}(B_k^T Q_j(r))\), a polynomial inequality after clearing \(D_r\);
(orbit \(e, g, a\)) \(F(Q_j(r)) {\lt} F(H^e Q_j(r) g_g)\), established through the term \(\operatorname{\mathrm{tr}}(B_a^T H^e Q_j(r) g_g) - [a = 4]\, \frac18\) with \(a \in \{ 0, 4\} \), again a polynomial inequality after clearing denominators, with the tabulated \(\hat g_g\) in place of \(g_g\) and an explicit error allowance.
If a domain leaf passes on a box, then no point of the box with \(u^2 + v^2 \le 1\) and \(|r_i| \le 2\) is reduced.