The mixed crossing sum is even and defines linking number

Let ${\gamma }_1,{\gamma }_2:S^1\to {\mathbb{R}}^2$ be the projected component maps. They are transverse at every mixed crossing by [F1]. The map $F:S^1\times S^1\to {\mathbb{R}}^2\times {\mathbb{R}}^2$, $F(s,t)=({\gamma }_1(s),{\gamma }_2(t))$, is transverse to the diagonal $\mathrm{\Delta }=\{(x,x):x\in {\mathbb{R}}^2\}$, and its inverse image of $\mathrm{\Delta }$ has one point for each mixed crossing because there are no triple points. Therefore $I_2(F,\mathrm{\Delta })$ is the number of mixed crossings modulo $2$. Homotope ${\gamma }_1$ linearly to a point $p$ with $\parallel p\parallel$ greater than ${\max }_t\parallel {\gamma }_2(t)\parallel$; the endpoint map misses $\mathrm{\Delta }$. By [F3], the intersection number is $0$, so the number of mixed crossings is even.

A type-I move contributes no mixed crossing because its new crossing is a self-crossing. Under type II, either both crossings are self-crossings or they are both mixed and have opposite signs by [F5], so $S(D)$ is unchanged. Under type III the three crossing signs and over/under data are preserved, so the mixed subset and its signed sum are unchanged. Planar isotopy creates no crossings and preserves the oriented crossing charts. Hence each move preserves $S(D)\mathrm{/}2$.

Each crossing sign is $+1$ or $-1$, both congruent to $1$ modulo $2$. Thus $S(D)$ has the same parity as the number of mixed crossings shown even in step 1.1; consequently $S(D)\mathrm{/}2$ is an integer. Swapping component labels leaves each mixed crossing unchanged, while reversing one strand orientation negates its tangent vector and hence the determinant in [F2]; reversing both vectors preserves the determinant. This proves symmetry and the orientation rules.

If two regular diagrams represent the same oriented link, [F4] gives a finite sequence of the moves and planar isotopies checked in step 1.2. By step 2.1 their half-sums are integers; step 1.2 preserves these values at every move, so the endpoint linking numbers agree. Countable Choice is used through [F3] for homotopy-invariant mod $2$ intersection and through [F4] for the finite-move reduction; the determinant calculations and the move-by-move checks are choice-free.