linkingComplementH1
plain-language theorem explainer
Content-typed first singular homology of the complement of a continuous map $S^1\to S^D$, valued in Mathlib's $\mathbb{Z}$-modules. Anyone citing the real linking obstruction (panel K1) or the $D=3$ bridge uses this object rather than an arithmetic encoding. The body is a direct application of Mathlib's singular homology functor to the complement subspace.
Claim. For $D\in\mathbb{N}$ and a continuous map $f:S^1\to S^D$, define the $\mathbb{Z}$-module $H_1\bigl(S^D\setminus\mathrm{im}(f);\mathbb{Z}\bigr)$ by applying Mathlib's singular homology functor in degree $1$ to the topological subspace of $S^D$ consisting of points outside the image of $f$.
background
PublicSpine is the public dual of UnifiedForcingChain: a $\delta$-stratified surface on which papers cite what is forced. Contract rule 3 bans encoding predicates for the T8/T7 bridge; linking must be stated on genuine Mathlib homology of complements, not on a name-firewall Prop.
The object here is exactly what Alexander duality computes for a circle in $S^D$: first singular homology with $\mathbb{Z}$ coefficients of the open complement. Upstream, $H_1(S^1;\mathbb{Z})$ has infinite order via the covering-space winding invariant (CircleWindingChain), and spatial dimension $D=3$ is the T8/T9 target in the forcing chain. The continuum and cost panels of this module are separate; this binder is only the content-typed linking carrier.
History (panel K1, 2026-07-08): an abstract detects : ℕ → Prop plus a not-encoding firewall was gameable both ways (empty detector inhabited it; funext/propext collapsed honest detectors to the encoding). Content-typing on the Mathlib object is the non-gameable form.
proof idea
Definition, not a proof. The body feeds the complement subspace ${x\in S^D\mid x\notin\mathrm{range}(f)}$ (as a TopCat object) into Mathlib's singularHomologyFunctor at coefficient ring $\mathbb{Z}$ and degree $1$, returning an object of ModuleCat ℤ. No lemmas are applied; noncomputable only because singular homology is.
why it matters
This is the carrier for the non-encoding detector: DetectsNontrivialLinking D asserts existence of an embedding $f:S^1\hookrightarrow S^D$ whose complement has non-zero $H_1$. That detector is restated verbatim in LinkingVanishingLowDim and LinkingVanishingHighDim, and is the content half of the closed Alexander linking bridge (campaign P-d3link, 2026-07-18) that forces $D=3$ without arithmetic encodings.
Downstream, UnknotComplementRetract uses the same shape for the unknot in $S^3$ (embedding plus complement retract). Framework landmark: T8 ($D=3$ spatial dimensions) and the eight-tick octave sit on this bridge; the module doc records the bridge as fully inhabited with axioms only propext, Classical.choice, Quot.sound. Without this content-typed object, T8 would still be certificate-only on the UFC Boolean spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.