Termination and exact validation of the triangulated-exterior chain procedure

There are finitely many edges, 2-simplices, meridian-loop edges, vertices, simplices, and face incidences in the finite input. Each validation pass performs finitely many additions and comparisons of integer vectors, so it terminates. It returns invalid-labeling at the first failed edge-reversal, face-sum, or meridian-image check; if none fails, it proceeds to construction. By [F1] there are no other label-rejection branches, so rejection occurs exactly for the stated failed checks.

By [A1] the 1-skeleton is finite and connected. The procedure scans its finite ordered edge list, adds an edge exactly when its endpoints lie in different current components, and merges those components. Each addition reduces the number of components by one; connectedness therefore yields a spanning tree after finitely many additions, with exactly $\mathrm{\mid }V\mathrm{\mid }-1$ edges. The paths in this tree have finite length, and the sum of their integer edge labels is a finite computation for each vertex. Each simplex has finitely many edges and faces, so the prescribed exponent and signed Laurent coefficient are computed by finitely many additions, comparisons, and table insertions. There are finitely many simplices, hence all boundary matrices are produced and the algorithm terminates with exactly the free modules and face-incidence entries in [F1].