The BMW braid-closure algorithm terminates and returns its stated value

The first branch tests the exact grammar and then the listed count and index conditions. By [F1], it returns REJECT exactly for the stated invalid cases, and an accepted string gives a finite signed braid word. Parsing a finite string terminates. For fixed $n$, there are finitely many matching connectors. By [F4], each connector has a standard descending class. For each matching, draw its finitely many open strands as simple polygonal arcs in $R$ with the fixed rational endpoints. Choose their interior vertices in general position and approximate them sufficiently closely by rational coordinates, preserving the endpoints and avoiding self-crossings, tangencies, and triple points. Assign each crossing so that the earlier strand is over the later one. This gives a rational generic descending code for the connector, so Step 3’s ordered search has a witness and terminates. Step 5 uses the explicit rational closure arcs $C_j$ in the algorithm. For $j<k$, $x_j<x_k$ and ${ϵ}_j>{ϵ}_k$, so their exterior lanes are nested and disjoint; they meet $R$ only at the prescribed endpoints. Thus each trace entry is a finite closed diagram without a closure-code search. The number of basis tangles and generator matrices is finite.

For each reducer input $D$, the Step 4 traversal is determined by the endpoint labels, retained segment labels, and current crossing or smoothing pairings. Thus the crossing count $r(D)$ and bad-crossing count $b(D)$ are well defined. At a terminal input, the algorithm reduces a crossingless tangle to its matching, simplifies a descending tangle leaf, or evaluates a descending closed diagram by its curls and free circles using [F2]. At a selected bad crossing, [F3] shows that switching keeps $r$ fixed and lowers $b$ by one, while either smoothing lowers $r$ by one. Every recursive child therefore has a smaller lexicographic pair.

Assume by strong induction that every reducer input with smaller pair terminates. Each recursive node has at most three children, and by [F3] every child has a smaller pair than its parent. Well-founded induction therefore gives a finite reduction tree for every generator-matrix column and every closed trace entry.

The recursive reductions apply the defining skein relation, and their terminal matching coordinates are unique by [F4]. Thus the finite matrix products give the coordinates of ${\mathrm{\Phi }}_n(b_{\beta })$ by [F5]. Pairing with the computed trace row yields $d^{-n}P(\widehat{{\mathrm{\Phi }}_n(b_{\beta })})={\tau }_n(b_{\beta })$ by [F2]. By [F6], the algorithm's $w,c$ are the determinant writhe and component count of this oriented closure. Under $a=-iA,z=iZ$, the relation $z(d-1)=a-a^{-1}$ becomes $Z(d-1)+A+A^{-1}=0$, and $q-q^{-1}=z$ becomes $q-q^{-1}=iZ$. The units $a,d,q$ map to units, so the substitution defines $\phi :T\to T_K$. Step 6 is a finite symbolic substitution followed by multiplication, returning exactly $-i^w(-1{)}^c{A}^{-w}\phi (d^{n-1}{\tau }_n(b_{\beta }))$. No division by $Z$ occurs.