8 Irrational data
The vertices of \(\operatorname{\mathbf{P}}\) and the symmetries \(g_k\) involve \(\cos (2\pi k/15)\) and \(\sin (2\pi k/15)\). The checker works with dyadic approximations of these numbers; this chapter bounds the approximation errors. Nothing else in the proof is irrational.
Let \(\theta _1 = 2\pi /15\). Then \(\theta _1 = \pi /3 - \pi /5\), and \(\cos \theta _1\) and \(\sin \theta _1\) are known to \(28\) decimal places.
\(\cos (\pi /5) = (1 + \sqrt5)/4\) and \(\sin (\pi /5) = \sqrt{10 - 2\sqrt5}/4\); expand \(\cos \) and \(\sin \) of the difference, and bound \(\sqrt3\), \(\sqrt5\) by rationals.
\(\sin (2\pi /15) \le \frac{57}{128} \cos (2\pi /15)\).
From the bounds of Lemma 57.
For \(k = 0, \dots , 14\), the checker’s tables of \(\cos (2\pi k/15)\) and \(\sin (2\pi k/15)\) (dyadic numbers with denominator \(2^{80}\)) are within \(2^{-71}\) of the true values.
Let \(z_k = e^{2\pi i k/15}\) and let \(\hat z_k\) be the table entry. Then \(|z_1 - \hat z_1| \le 2^{-79}\) by Lemma 57, and \(z_{k+1} = z_k z_1\), so \(|z_{k+1} - \hat z_{k+1}| \le |z_k - \hat z_k| + |\hat z_k|\, 2^{-79} + |\hat z_k \hat z_1 - \hat z_{k+1}|\). The last two terms are computed exactly in \(\operatorname{\mathbb {Q}}\) and are at most \(2^{-75}\) for each \(k\), so \(|z_k - \hat z_k| \le k\, 2^{-75}\).
Every coordinate of every tabulated vertex is within \(2^{-60}\) of the corresponding coordinate of the true vertex of \(\operatorname{\mathbf{P}}\).
The points \(C_1, C_2, C_3\) are rational and tabulated within \(2^{-80}\). A vertex is \(\pm R_z(2\pi k/15) C_i\); the error of a product of approximations is bounded by the sum of the errors, since all factors are bounded by \(1\).
Every entry of every tabulated rotation \(\hat g_k\) is within \(2^{-60}\) of the corresponding entry of \(g_k = R_z(2\pi k/15)\).
Immediate from Lemma 59.
The pairing used in the blow-up of chart 4 is exact: \(\tau \) maps true vertices to true vertices (Lemma 28), and the blow-up bracket \(L\) is linear in \(S\), so the same vertex error bound applies to it.