Termination, correctness, and bounds of normal-surface unknot recognition

The given countable-choice hypothesis [A1] supplies the choice assumption in [F5]. That item constructs a finite good exterior triangulation with $t\le C(n+1)$ tetrahedra and a marked original meridian; the zero-crossing case uses its fixed product model. By [F1], validation and either search mode terminate.

For Haken mode, the box has $(t{2}^{7t+2}+1{)}^{7t}=2^{O(t^2)}$ vectors. Testing fundamentalness checks at most the same number of coordinatewise decompositions per vector, so the squared count remains $2^{O(t^2)}$; all tests on each compressed vector take polynomial time. Store only the current vector, one decomposition vector, counters and the matching matrix, using $O(t^2\log (t+2))$ bits.

For JT mode, the support enumeration has at most $2^{7t}$ subsets. Use the streamed modular rank/kernel implementation [F7], whose prime bound and stopping rule give polynomial bit time and $O(t^2\log (t+2))$ workspace for each support. The candidate tests use polynomial time in $t$ and the $O(t)$-bit coordinates from [F6], giving total $2^{O(t)}$ time. The implementation reuses one residue matrix and a bounded CRT accumulator, while the candidate and support counter fit within $O(t^2\log (t+2))$ bits; no list of prior rays is stored because each ray is enumerated at its exact zero support.

Account also for preprocessing in [F8]. On a valid $n$-crossing code, the crossing, incidence and face tables have $O(n)$ entries of $O(\log (n+2))$ bits. The syntax, permutation-orbit and component checks use polynomially many table scans. To find the lexicographically first spanning tree, even exhaustive testing of the at most $2^{2n}$ edge subsets suffices, with one subset and one connectivity table stored at a time; this uses $2^{O(n)}$ bit time and $O(n\log (n+2))$ space. The returned crossing-disk, band and face-cap record has $O(n)$ total port occurrences. Applying its fixed triangulation, prism, coning and tube templates produces the combinatorial exterior and meridian tables of [F5] with $O(n)$ cells and labels of $O(\log (n+2))$ bits. Fixed subdivisions multiply this count only by constants. Generating and matching these lists by repeated scans takes polynomial bit time and $O(n\log (n+2))$ storage. Thus preprocessing fits both stated search bounds; the code-only computation uses these finite incidence records.

The compressed disk tests also have the claimed polynomial resource cost. Let $f={\sum }_i{v}_i$ be the disk count, $a={\sum }_i{q}_i{v}_i$ the total side count, where $q_i$ is three or four, and $b$ the count of sides in boundary faces. Choose one incident tetrahedron at each global edge and sum its local disk-intersection counts to obtain the surface vertex count $c$. Matching makes these edge counts consistent. Then $\chi =c-(a+b)\mathrm{/}2+f$, and the boundary is nonempty exactly when $b>0$. The meridian edge path crosses the boundary normal curves away from triangulation vertices; its intersection parity is the sum, with path multiplicity modulo two, of their counts on its edges. These are linear sums of $O(t)$-bit coordinates over polynomially many incidences. They take polynomial bit time and fit the stated workspace. Connectedness is supplied by fundamentalness in either branch, so no expanded surface is stored. Together with the separately counted decomposition and rank tests, this justifies the candidate-test costs in steps 1.2–1.3.

In Haken mode, [F2] identifies acceptance exactly with existence of an essential disk in that exterior; by [F4], this is equivalent to the smooth knot being the unknot. In JT mode, the same conclusion follows from [F3] and [F4]. Thus each terminating branch returns the correct decision using the proved Haken and JT existence suppliers.

Substituting $t\le C(n+1)$ in steps 1.2–1.3 and including the preprocessing and compressed tests of steps 1.4 and 2.1 yields the stated time and space bounds; the fixed $n=0$ branch is constant size.