Reduced Khovanov homology over F2 is an oriented link invariant

By [F0], the based reduced groups in the Statement are defined for diagrams of every nonempty oriented link. For any two such diagrams $D,D^{\mathrm{\prime }}$, [F1] gives a finite sequence $D=D_0,D_1,\dots ,D_r=D^{\mathrm{\prime }}$ of planar isotopies and oriented Reidemeister moves. For a Reidemeister step choose a marked point on an unchanged exterior arc and carry it to the corresponding arc on the other diagram. Such an arc exists: the move models contain a continuing strand meeting the boundary of their disk, and a closed regular link diagram continues that strand outside the disk. For a planar isotopy choose any mark and carry it by the isotopy. There are finitely many steps and every diagram is nonempty, so these are finite point choices, adding no choice hypothesis beyond [F1]. These auxiliary marks need not all lie on a single tracked component.

At the start of a step, [F3] identifies the current reduced group with the reduction at its chosen auxiliary mark, even if that mark lies on another component. For a Reidemeister move, [F2] then gives a bigraded cochain homotopy equivalence between the reductions at the two unchanged exterior marks. Its integral maps and contractions commute with the marked action before quotienting, and their explicit equations remain true over ${\mathbb{F}}_2$. For a planar isotopy the relabeling of circles preserves that marked factor and every normalized degree. Thus each step supplies a bigraded cohomology isomorphism, followed if necessary by another fixed-diagram change of mark using [F3].

Compose these finitely many isomorphisms, using [F3] at the first and last diagram to reach the originally selected marks. This proves independence of the diagram and chosen component. For an empty move sequence only [F3] is needed. Each vector space has finite support in its bigrading, so finite choices of its isomorphisms assemble the asserted noncanonical bigraded isomorphism. The proof uses neither a canonical identification of different move sequences nor a relative movie theorem for multi-component cut tangles. ACω is used only in [F1]; the local tensor equations and fixed-diagram mark changes are finite and choice-free.