H1_complement_isZ
plain-language theorem explainer
Predicate selecting dimensions where the first homology of a circle complement in the D-sphere is infinite cyclic. It is the Alexander-duality form of the loop-loop linking condition, not a bare equality D = 3. Anyone specializing same-sector linking to p = 1 (the T-step that forces three spatial dimensions) cites it. The body is a one-line alias of the circle-linking cohomology predicate.
Claim. For $D \in \mathbb{N}$, write $H_1\_\mathrm{complement\_is}\,\mathbb{Z}(D)$ for the assertion that $S^D$ admits nontrivial linking of disjoint embedded circles. Equivalently (Alexander duality), the reduced cohomology $\tilde H^{D-2}(S^1)$ is nontrivial, which holds exactly when $D = 3$.
background
Module U5 formalizes the topological (T) specialization of same-sector linking. For loop-loop linking one takes $p = 1$; Alexander duality then says $H_1(S^D \setminus K) \cong \mathbb{Z}$ if and only if $D = 3$. The genuine cohomology computation lives in Foundation.AlexanderDuality; this module only packages the selector used by the verification spine.
Upstream, SphereAdmitsCircleLinking D is defined as CircleReducedCohomologyNontrivial (D - 2). By Hatcher Thm 3.44, linking of circles in $S^D$ is nontrivial precisely when $\tilde H_1(S^D \setminus S^1)$ is nontrivial, and that group is isomorphic to $\tilde H^{D-2}(S^1)$. The reduced cohomology of $S^1$ is nontrivial only in degree 1, forcing $D - 2 = 1$.
Same-sector arithmetic alone still permits every odd $D \ge 3$; the loop-loop conclusion $D = 3$ is the $p = 1$ specialization. Constants modules pin the forced spatial dimension as the literal 3 once this selector fires (T8 in the forcing chain).
proof idea
Pure definitional alias: the body is exactly SphereAdmitsCircleLinking D. No tactics, no lemmas applied at this site. All mathematical content is deferred to the Alexander-duality predicate, which itself reduces to nontriviality of $\tilde H^{D-2}(S^1)$.
why it matters
Closes the U5 packaging step: the linking selector no longer hard-codes D = 3 but names the cohomology condition that forces it. Downstream siblings (loop_loop_linking_forces_D3, the witness family witness_D3/D5/...) and the T6-T8 spine audit rely on this name to keep the (T) specialization honest. In the Recognition forcing chain this is the topological half of T8 (three spatial dimensions): once loop-loop linking is required, Alexander duality collapses the odd-dimension ladder to $D = 3$. The module also prepares U10 (nontriviality witnesses for the converse $A_A = {3,5,7,\ldots}$), where the same selector distinguishes the $p = 1$ case from higher odd dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.