zSeg_cycle
plain-language theorem explainer
If a singular 1-chain is a cycle in the complement of a full arc on the D-sphere, its pushforward into the complement of any parameter subsegment remains a cycle. Used by the bisection argument for arc-complement acyclicity. Proof is a one-line application of the general fact that chain maps send cycles to cycles.
Claim. Let $a$ be a continuous arc on the sphere $S^D$ and let $z$ be a singular $1$-chain in the complement of the image of $a$ with $\partial z=0$. For any real parameters $u,v$, writing $z_{u,v}$ for the pushforward of $z$ along the inclusion of that complement into the complement of the image segment $a([u,v])$, one has $\partial z_{u,v}=0$.
background
The module develops singular-chain tools for complements of arcs on the $D$-sphere, with $D=3$ the spatial dimension forced by the Recognition Science chain (T8). Chains live in the coproduct presentation Cgrp, and bnd X n is the singular boundary $C_{n+1}(X)\to C_n(X)$.
An arc $a$ maps the unit interval into $S^D$. For parameters $u,v$, seg a u v is the image $a([u,v])\subseteq S^D$. The reference cycle $z$ lives in the complement of the full image of $a$. The restricted chain zSeg a z u v is the pushforward of $z$ along the inclusion of that full-arc complement into the (larger) complement of the smaller segment $a([u,v])$.
Upstream, chainMap_cycle records that continuous maps induce chain maps sending cycles to cycles: if $\partial z=0$ then $\partial(f_\sharp z)=0$. That is the only algebraic input here.
proof idea
One-line term proof. By definition zSeg is the degree-1 chain map of the inclusion of the full-arc complement into the segment complement, applied to $z$. Apply chainMap_cycle to that inclusion and the hypothesis $\partial z=0$; the conclusion is exactly $\partial(\mathrm{zSeg},z)=0$.
why it matters
Feeds bad_step, the bisection step: a "bad" parameter interval (one whose restricted pushforward is a nonbounding cycle) has a bad half of half the length. That step is the inductive engine of the arc-complement acyclicity argument in this module.
Arc-complement acyclicity is the topological half of the linking-vanishing package imported from LinkingVanishingHighDim. In the Recognition forcing chain, nontrivial linking of closed curves forces spatial dimension $D=3$ (T8); the complement of an embedded arc must not support a nontrivial $1$-cycle that would obstruct the linking calculus. This lemma keeps the cycle property alive under interval restriction so the bisection can run.
No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.