unknotComplementH1_ne_zero
plain-language theorem explainer
Given $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, the first singular homology of the flat unknot complement in $S^3$ is not the zero module. Anyone proving DetectsNontrivialLinking at dimension 3 cites this. The argument is a pure retract: the dual core circle and its retraction make $H_1(S^1)$ a retract of the complement's $H_1$, so vanishing of the latter forces $\mathbb{Z}=0$.
Claim. Assume the first singular homology of the circle with integer coefficients is isomorphic to $\mathbb{Z}$ as a $\mathbb{Z}$-module. Then the first singular homology (with $\mathbb{Z}$ coefficients) of the complement in $S^3$ of the standard flat unknot $S^1\hookrightarrow S^3$, $(x_0,x_1)\mapsto(x_0,x_1,0,0)$, is not the zero object in $\mathbf{Mod}_{\mathbb{Z}}$.
background
This module is the geometric core of nontrivial-linking detection in dimension 3. It builds, over Mathlib only, the flat unknot as a continuous embedding $S^1\to S^3$, the dual core circle valued in the complement, and a continuous retraction of the complement onto that core, with the composite along the core equal to the identity on $S^1$.
The complement is the subtype of $S^3$ of points outside the image of the unknot. The core map sends $z\mapsto(0,0,z_0,z_1)$ into that complement; the retraction normalizes the last two coordinates. Singular homology is Mathlib's singularHomologyFunctor with coefficients in $\mathbb{Z}$, evaluated in degree 1.
Upstream, the identity-on-core fact (retract_core) and the continuous core map into the complement are the geometric inputs. The numerical contradiction at the end uses that $1\neq 0$ in $\mathbb{Z}$.
proof idea
Assume for contradiction that $H_1$ of the complement is the zero object. From the given iso, $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Let $g$ be the core inclusion $S^1\to$ complement and $r$ the retraction back; the geometric identity $r\circ g=\mathrm{id}_{S^1}$ is retract_core.
Functoriality of degree-1 singular homology yields $H(g);H(r)=\mathrm{id}$ on $H_1(S^1)$. Zero-target forces $H(g)=0$, hence $\mathrm{id}=0$ on $H_1(S^1)$, so that object is zero. Transport along the given iso makes $\mathbb{Z}$ zero as a module, hence a subsingleton, contradicting $1\neq 0$.
why it matters
This is the capstone of the unknot-complement retract module and the geometric half of linking detection at $D=3$. Downstream, detectsNontrivialLinking_three packages the unknot embedding with this nonvanishing (fed the circle homology iso) to discharge DetectsNontrivialLinking 3: "the detection half is proved (R2 of campaign P-d3link)".
In the Recognition forcing chain, T8 forces three spatial dimensions; nontrivial linking of $S^1$ in $S^3$ is the topological signature that the ambient dimension is high enough for genuine linking. The argument uses real Mathlib singular homology throughout, with no arithmetic encoding.
The axioms audit on the built module reports only propext, Classical.choice, and Quot.sound: no new axioms. The remaining external input is the hypothesis that $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, supplied downstream by the circle-winding chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.