Enumeration up to a crossing bound procedure properties

Fix $c\ge 1$. There are $2^c$ crossing-sign vectors. Each vector has exactly $2c$ outgoing and $2c$ incoming darts by [F1], so it has $(2c)!$ bijections between them. Every resulting edge involution has $4c$ darts, hence at most $4c$ face cycles because its cycles are nonempty and disjoint. The number of candidate records considered at this $c$ is therefore at most $2^c(2c)!(4c)$. At $c=0$ the two orientation markers in [F4] give exactly two crossingless codes. Summing these finite bounds over $0\le c\le N$ proves that all loops and validator calls are finite; each validator call terminates by [F3].

Every appended record is produced from a normalized code in the finite loops. It is appended only when the validator returns Valid and its component tracing has exactly one cycle. By [F3] this code is connected, has the required face count and outer face, and reconstructs the corresponding decorated diagram. Conversely, consider any normalized connected one-component code with $c\le N$. Its signs occur in the enumerated sign-vector list. Its edge involution pairs each outgoing dart with one incoming dart, so it is one of the enumerated bijections; its selected outer face is one of the enumerated face cycles. Canonical edge labels in [F1] then give exactly that normalized code. The validator returns Valid by [F3], and its one component passes the final filter, so the candidate is appended. At $c=0$, each of the two orientation markers in [F4] is among the initial candidates.

The procedure's only equivalence-related operation is the fixed label normalization in [F1]. It performs no test between two returned diagrams and removes no candidates on the basis of planar isotopy or ambient isotopy in $S^3$. Thus the exact output is the finite list of reconstructed code candidates, with possible repeated knot types, not a classification of knot types.