not_detectsNontrivialLinking_zero
plain-language theorem explainer
At dimension zero, no continuous embedding of the circle into the two-point 0-sphere leaves a complement with nontrivial first homology. Citers of the D=3 linking force (campaign P-d3link, vanishing half R3a) need this base case. The proof is a one-line re-export of the low-dimension vanishing lemma on totally disconnected subspaces of S⁰.
Claim. There is no continuous embedding $f\colon S^1\hookrightarrow S^0$ such that the first singular homology of the complement $S^0\setminus f(S^1)$ is nonzero. In other words, the non-encoding linking detector fails at dimension $0$.
background
PublicSpine is the public dual forcing surface of UnifiedForcingChain: a δ-stratified map that papers should cite for what is forced. Its closed D=3 / 8-tick bridge target is AlexanderLinkingBridge (campaign P-d3link), assembled from detection at D=3, CubePeriodEight, vanishing at D=0 and D=1, and forcing away from D=2 and D≥4.
The detector here is the non-encoding predicate: some continuous embedding of the circle into the D-sphere whose complement has nonvanishing first singular homology (Mathlib object, not an arithmetic encoding). At D=0 the ambient space is the two-point 0-sphere. Every subspace of a totally disconnected space is totally disconnected, so complement H₁ vanishes for any map from S¹.
Upstream, LinkingVanishingLowDim restates the same detector and proves the D=0 case; the high-dim twin handles D≥4 via arc-complement acyclicity.
proof idea
One-line term wrapper: apply LinkingVanishingLowDim.not_detects_zero, which already shows the detector fails at dimension 0. No local algebraic work; the content lives in the low-dim vanishing module (totally disconnected S⁰ implies empty or discrete complements, hence vanishing H₁).
why it matters
Closes the D=0 vanishing half of R3a in campaign P-d3link, one of the four pieces that inhabit AlexanderLinkingBridge on this public spine (with d3_detects, CubePeriodEight, D=1 vanishing, and forces_D3 for the remaining dimensions). That bridge is the honest content-typed binder for T8 (spatial dimension D=3) and the eight-tick octave target; the module doc records it CLOSED with zero sorry and only standard classical axioms.
Without vanishing at 0 and 1, the detector could hold in low dimension and the force-to-three argument would not pin D=3. Downstream used_by is empty on this page, but the declaration is part of the public spine package that papers and loops must cite for the linking force rather than UFC certificate names.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.