Finite procedure properties of the Haken–Jaco–Tollefson search

The code and each encoded field are finite, so the planar-code validation procedure terminates. Its prescribed return is passed through unchanged; a valid multi-component code returns not-a-knot immediately. For a valid one-component code, the good exterior triangulation is a finite combinatorial output by [F1].

In Haken mode the integer bound $B=t{2}^{7t+2}$ is finite and nonnegative, so the lexicographic box contains exactly $(B+1{)}^{7t}$ vectors. Each matching, quadrilateral, and disk test scans finite coordinates and faces. Fundamentalness is decided by checking every coordinatewise split $v=x+(v-x)$; there are at most ${\prod }_i(v_i+1)$ such splits, each tested by finitely many integer comparisons. Therefore every loop and the complete Haken search terminate.

In JT mode there are exactly $2^{7t}$ subsets $Z$. For each, computing the rank and, when the nullity is one, an integer kernel generator by exact finite matrix operations terminates. Checking admissibility, deduplicating, and testing the boundary data are finite scans. Thus the complete JT search terminates.

The algorithm's ordered validation branch returns its first invalid result; its component branch returns not-a-knot exactly for a valid multi-component input. In either one-component mode, all candidates are drawn from the stated finite enumeration and a return of no-candidate occurs only after that enumeration ends. Steps 1.1–1.3 prove the stated termination and output form.