zSeg
plain-language theorem explainer
Defines the degree-1 singular chain obtained by pushing a fixed reference cycle on the full arc complement forward into the complement of a parameter subsegment a([u,v]) on S^D. Used throughout the bisection argument for arc-complement H_1-acyclicity (Hatcher 2B.1). Construction is the chain map of the complement inclusion induced by seg ⊆ range(a).
Claim. For real parameters $u,v$ and a fixed reference $1$-cycle $z$ on the complement of the full arc image in $S^D$ ($D=3$), let $z_{\mathrm{seg}}(u,v)$ be the image of $z$ under the chain map induced by the continuous inclusion of the full-arc complement into the complement of the closed subarc $a([u,v])$.
background
The module develops a formal version of Hatcher's arc-complement acyclicity: every topological embedding $a:I\hookrightarrow S^D$ has $H_1$-acyclic complement. Spatial dimension is fixed at $D=3$ (T8/T9 forcing). The ambient space is the unit sphere $\mathrm{Sph},D$.
A parameter subinterval yields the closed subarc image $\mathrm{seg}(u,v)=a({q\in I:u\le q\le v})$, which sits inside the full arc range. The map $\mathrm{cInc}$ is the continuous inclusion of the complement of a larger set into the complement of a smaller one; here it is applied to $\mathrm{seg}\subseteq\mathrm{range}(a)$. Singular chain groups are written $\mathrm{Cgrp}(X)_n$, and $\mathrm{chainMap}$ is the induced map on chains.
The reference cycle $z$ lives in degree 1 on the full-arc complement and is assumed closed (boundary zero) in the lemmas that consume this definition.
proof idea
One-line definitional wrapper: apply the degree-1 chain map of $\mathrm{cInc}(\mathrm{seg_subset_range},a,u,v)$ to the fixed reference cycle $z$. No further algebraic work; naturality and cycle preservation are proved separately as $\mathrm{zSeg_cycle}$ and $\mathrm{zSeg_restrict}$.
why it matters
This is the movable $1$-cycle that the bisection invariant tracks. Downstream, $\mathrm{Bad}(u,v)$ asserts that $[u,v]\subseteq[0,1]$ and that $z_{\mathrm{seg}}(u,v)$ is not a boundary; $\mathrm{bad_step}$ halves a bad interval while preserving non-bounding; $\mathrm{zSeg_cycle}$ and $\mathrm{zSeg_restrict}$ keep the class closed and compatible under nested segments. Those pieces feed the contradiction argument in $\mathrm{arcComplementsAcyclic}$ (Hatcher 2B.1, arc case): if the full-arc complement had nontrivial $H_1$, nested bisection would produce a point whose complement still carries a nonbounding cycle, which is impossible. In the Recognition forcing chain this underwrites linking vanishing in $D=3$ (T8/T9), the geometric input that forces three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.