The boundary intersection pairing is well defined and rationally nondegenerate

Given: Full AC and a compact connected oriented smooth four-manifold $W$ with $\mathrm{\partial }W=M$ and $H_{\ast }(M;\mathbb{Q})\cong H_{\ast }(S^3;\mathbb{Q})$.

The long exact sequence of the pair contains $H_2(M;\mathbb{Q})\to H_2(W;\mathbb{Q})\to H_2(W,M;\mathbb{Q})\to H_1(M;\mathbb{Q})$. Both end groups vanish by the boundary hypothesis. Long exact sequence of a pair

Poincaré–Lefschetz duality identifies $H_2(W,M;\mathbb{Q})$ with $H^2(W;\mathbb{Q})$. Poincaré–Lefschetz duality

Over the field $\mathbb{Q}$, the universal-coefficient theorem identifies $H^2(W;\mathbb{Q})$ with ${\mathrm{Hom}}_{\mathbb{Q}}(H_2(W;\mathbb{Q}),\mathbb{Q})$. The universal coefficient theorem for cohomology over a PID

Double $W$ along a boundary collar; the resulting closed smooth manifold has finite CW homotopy type under full AC. Folding the second copy into the first makes $W$ a homotopy retract of the double, so $H_2(W;\mathbb{Z})$ is a direct summand of a finitely generated group. Collar neighborhood theorem A closed smooth manifold has the homotopy type of a finite CW complex

The boundary intersection form is the signed intersection pairing on interior representatives. Intersection lattice of a four-manifold with rational-homology-sphere boundary

Full AC is assumed for the finite-CW homotopy-type supplier [F4].