Valid codes reconstruct the declared link diagram

By validity, the code passes every finite check in [F3]. If $c=0$, [F1] gives the one-component crossingless code and its cw or ccw orientation; [F2] realizes that oriented code as the standard circle with the outside face selector. If $c>0$, its one component satisfies the knot-code condition, and the face-count hypothesis in [F2] yields a spherical crossing graph with the prescribed rotations and edge pairings; deleting a point in the selected face gives its plane model. Replace each crossing disk by the prescribed smooth transverse crossing, choosing the ports and collars so the edge-band centerlines join their crossing strands tangentially. Away from the crossing disks, round the finitely many polygonal bends in pairwise disjoint neighborhoods that meet no other edge portion. On each over-strand set the height to $+1$ and on each under-strand set it to $-1$ near every crossing; along each edge interval interpolate smoothly between its prescribed endpoint heights, constant near those endpoints. The resulting projection is a smooth immersion with exactly the prescribed finite transverse double points and no triple points. Its only repeated projected points are crossing pairs, and those pairs have distinct heights, so the lift is a smooth embedded link in $S^3$. Thus the procedure's plane model is a regular oriented diagram by [F3] representing the input code.

Suppose $c>0$. At each double point the two branches are smooth and transverse. Smooth local defining functions for them have independent differentials, so together form coordinates in which the branches are the coordinate axes. Corresponding oriented branch germs and cyclic orders give orientation-preserving matching crossing charts. Take disjoint small crossing disks in these charts. Each edge left after truncation is a compact embedded interval; a strip coordinate along it can be chosen to agree with the crossing coordinates near both ends. Explicitly extend the end longitudinal parameters increasingly along the interval, and extend their transverse coordinate vector fields by finitely many convex combinations of fields pointing to the same side; these combinations stay transverse. Short flows give the strip, and compactness supplies a common width. Shrink the finitely many widths to avoid all other truncated edges and crossing disks except their assigned end collars. This construction treats different endpoint germs separately, so it applies to loops and parallel edges as well. Using the same abstract disk-and-band model in the two drawings gives a smooth diffeomorphism of their graph neighborhoods $N_0,N_1$ carrying vertices, edges, strand orientations, and crossing decorations as prescribed. Round corresponding boundary corners in the same model; the map is then smooth across all joins and carries their smooth boundary circles to the matching circles. These circles correspond to the same face cycles, even when a facial walk repeats a cut vertex.

Relabel the finite crossing set in increasing order and assign edge labels by the canonical scan in [F1]. The selected face is represented by the least dart of its face cycle. These are exactly the normalization rules used by the bounded enumerator. The resulting code has $c$ crossings, so it occurs in the enumerator's finite loops at bound $c$; [F4] then guarantees that its reconstruction is returned.

Regard the drawings and neighborhoods as subsets of the oriented sphere. Every complementary component of a connected neighborhood $N_i$ is a smooth disk. Indeed [L1] gives its bounded disk in a stereographic chart; choosing a second stereographic chart with its removed point inside that disk presents the other side as a bounded smooth Jordan region, also a disk by [L1]. The connected set $N_i$ lies on its collar side, so the other disk misses $N_i$; it contains no other boundary component, since that component's neighborhood collar would put $N_i$ on the other side. Thus it is a whole complementary component, and all components arise this way. Extend the neighborhood diffeomorphism over each pair of matching disks by [L1], using collars induced by its smooth extension across their boundary germs. Such a germ extension exists in the local smooth boundary charts, and has positive normal derivative; finitely many charts and a smaller collar retain smoothness and invertibility. Hence the extended maps agree on actual collars, and the finite gluing is a smooth orientation-preserving sphere diffeomorphism. The selected outer face matches the disks containing infinity. When extending this pair, also prescribe the identity germ at infinity using the interior clause of [L1]. To apply that lemma, view each complementary disk in a stereographic chart whose removed point lies in its own neighborhood $N_i$; for the outer pair, the prescribed coordinate germ is the expression of the sphere's identity near infinity in these two charts. The resulting sphere diffeomorphism fixes a neighborhood of infinity. Its plane restriction $H$ is therefore an orientation-preserving smooth diffeomorphism carrying the two decorated diagrams.

If $c=0$, the two diagrams are smooth embedded circles with the same cw or ccw orientation marker. Choose an orientation-preserving diffeomorphism of their bounded disks using [L1]; its boundary map carries the circle orientations because these markers agree. Extend across the exterior disks on the sphere by [L1], matching the induced boundary collars and prescribing the identity germ at infinity as in step 2.2. This again produces an orientation-preserving plane diffeomorphism $H$ carrying the oriented diagram and its selected exterior face.

Finally every orientation-preserving smooth plane diffeomorphism $H$ is joined to the identity by a jointly smooth path of plane diffeomorphisms. Write $b=H(0)$ and $A=DH(0)$, and set $J_t(x)=(H(tx)-b)\mathrm{/}t$ for $t>0$, $J_0(x)=Ax$. The identity $J_t(x)={\int }_0^{1}DH(stx)xds$ proves joint smoothness at $t=0$. For $t>0$ the map is a composition of diffeomorphisms, and $J_0$ is the invertible positive linear map $A$. Join the identity to $A$ by polar decomposition: the positive definite factor is joined linearly to the identity, and the rotation factor by interpolating its angle. Follow that path by $J_t$ from $A$ to $H-b$, then by translations from $H-b$ to $H$. Smooth time reparametrizations constant near all joins give a jointly smooth ambient isotopy starting at the identity and ending at $H$. By steps 2.2 and 3.1 its terminal map transports the strand orientations and over/under data, so it is a planar isotopy in [F5]. Together with reconstruction and enumeration in steps 1.1 and 2.1 this proves every clause. Countable Choice is used only through [L1] for the smooth uniqueness construction; finite realization and enumeration retain their choice-free proofs.