The decorated knot Floer cobordism map

Choice scope. Fix the actual compact smooth cobordism, decoration, Spin-c structure and, for a comparison, the two actual decompositions. A compact smooth input has finite atlas/handle data. A Morse decomposition has finitely many critical points; a generic Cerf comparison has finitely many exceptional times (Zemke Lemma 11.18, p.80, and Theorem 11.5, pp.74 and 84–85). Choosing a finite list of charts, gradient-like fields, band neighborhoods, puncturing balls and standard auxiliary classes uses finite choice only. No choice of one decomposition for every cobordism is required: existence and pairwise comparison are quantified separately for arbitrary given inputs.

The dividing surface and boundary data meet the source category in [F1]: basepoints alternate, the dividing set separates the two regions, every three-manifold component meets the link, and every four-manifold component meets the divided surface. Closed dividing curves are allowed by its properly embedded one-manifold definition. The two-color assignment in [F3] is compatible on every elementary piece, including multicomponent and multiply based intermediate links. Its curvature is zero, so the imported curved maps are genuine maps of complexes over ${\mathbb{F}}_2[U,V]$.

Use the elementary maps of [F1] for the chosen parametrized Kirby decomposition, with [F2]'s actual auxiliary cycles and the fixed restricted Spin-c labels. Their finite polynomial counts, chain-map property and compatibility with the natural Heegaard transition maps are supplied by that external construction. Thus their composition is the displayed representative. If a component has an empty incoming or outgoing end, apply [F1]'s standard puncturing prescription before composing, not an undefined intermediate empty-link Heegaard diagram. No graph-TQFT reduction or hat-only construction is substituted for this two-variable map.

For that finite list of diagrams, the homotopy and periodic-domain data are countably indexed: use the finite-cell models of the compact manifolds and finite products of circles, and integer words in their finite attaching data; Spin-c extensions form a subset of a finitely generated integral cohomology torsor. Integer degrees, multiplicities, polygon types and neck lengths in $\mathbb{N}$ are countable indices as well. The count theorem [F4] supplies coherent perturbations relative to faces and fixed ends, rather than making independent choices at every real parameter value. Model counts and the finite move identities of [F1] use such zero- and one-dimensional polygon families; the elementary top classes in [F2] are algebraic classes on specified standard diagrams. A cycle representative, if needed, may be selected as the first representative in the explicit enumeration of finite polynomial chains over the countable ring. Nonempty single choices and finite choices require no additional axiom; countably many choices are covered by the assumed Countable Choice.

The geometric generic functions and comparison families can be chosen in the separable smooth spaces on those finitely many compact charts, with their countable derivative seminorms. Their residual conditions are indexed by countable jet charts/exhaustions, the finite singularity types and the countable curve classes; the analytic regularity choices are already furnished by [F4]. For the geometric Baire choices one may recursively select the first basic ball whose closure lies in the preceding ball and in the next dense open set, with diameters tending to zero. Completeness supplies the limit, so this step requires no choice over an uncountable set of functions. Source model relations are imported as finite geometric/count identities, with these actual CC-regular counts; their use does not require a well-ordering of all diagrams or a full-Choice selection of a global transitive system. Consequently the external proof specializes to the declared CC setting. This is a bounded choice inventory of its use here; it is not a claim that the publication itself discusses foundational optimality.

The distinguished class notation in the formula never selects a canonical cycle on every diagram: choose a representative on the actual standard auxiliary pair and carry it by the transition maps. Its boundary ambiguity is exactly the homotopy in [F2]. The local analytic triangle theorem supplies its own weighted bilinear identity, but the existence and correctness of the required elementary inputs come from [F1]–[F2]. Independence of all chosen decomposition data and the Spin-c extension sum are established in the separate naturality lemma by the external Theorems A and B.