Planar-code validation and reconstruction procedure properties

The input records are finite. Each label count, vector check, incidence count, and crossing check scans a finite list. Each component traversal marks at least one previously unvisited outgoing dart until it closes or reports a repeated/missing dart; since there are finitely many darts, it makes at most $\mathrm{\mid }D\mathrm{\mid }+1$ such visits. The crossing-connectivity scan uses the finite vertex and edge lists, and the face computation iterates a permutation of finite $D$, so it lists at most $\mathrm{\mid }D\mathrm{\mid }$ face cycles. The spanning-tree selection and disk/band construction use finite edge lists. If $c=0$, the separate branch ends after a finite comparison with its six allowed format-and-orientation combinations. Thus every input reaches a return after finitely many operations.

Every Invalid return is made immediately after its named predicate fails, and the procedure reaches predicates in the displayed order. Hence the returned reason and witness identify the first failed check. Conversely, if a finite input fails one of the stated checks, the finite scan reaches the first such failure and returns the corresponding invalid record before any later check.

Suppose a nonempty input passes the code-format, incidence, valence, strand, over/under, crossing-sign, component, and connectedness checks. Its finite tables then define the fixed-point-free edge involution $\alpha$, the clockwise crossing rotation $\sigma$, and the face permutation $\varphi =\alpha \circ \sigma$. The procedure's face scan lists exactly the cycles of this permutation by finite orbit tracing. It accepts the face stage precisely when their count satisfies $V-E+F=2$ and the supplied outer-face identifier names one of those cycles. By [F3], these conditions are necessary and sufficient for the spherical model, and deleting a point in the selected face gives the plane diagram returned in the output record.

In the crossingless branch, the accepted forms are exactly the six format-and-orientation combinations in [F4], with outer-face marker outside, representing its two normalized one-component codes. The local realization in [F3] realizes each marked orientation by a circle with two sphere faces; every other zero-crossing input, including one with a different outer-face marker, is rejected by the preceding branch checks. The nonempty and crossingless branches exhaust the possible nonnegative values of $c$, so the procedure terminates and has exactly the stated rejection and acceptance behavior.