bounds_of_halves
plain-language theorem explainer
A 1-cycle in the complement of a closed union KU = KP ∪ KM bounds whenever its pushforwards bound in each half-complement and H₂ of the midpoint complement vanishes. Arc-complement acyclicity arguments cite it as the algebraic half of geometric bisection. The proof transports the cycle across a homeomorphism to a Mayer–Vietoris cover, applies elementwise MV injectivity, and pulls the bound back along the retraction.
Claim. Let $W$ be a topological space and $K_P,K_M,K_U\subseteq W$ with $K_P,K_M$ closed and $K_U=K_P\cup K_M$. Suppose $H_2((K_P\cap K_M)^c)=0$. If $z$ is a $1$-cycle in $W\setminus K_U$ whose images under the inclusions of complements bound in $W\setminus K_P$ and in $W\setminus K_M$, then $z$ itself bounds in $W\setminus K_U$.
background
The module develops singular-chain tools for complements of arcs in spheres, aimed at showing that an embedded arc in $S^D$ has acyclic complement in low degrees when $D$ is large enough (linking forces $D=3$ in the RS forcing chain). Chains live in the singular complex $C_\bullet$, with boundary maps $\partial$ and induced chain maps along continuous maps of spaces.
Two local lemmas set the stage. Bounding pulls back along a retraction: if $f\circ g=\mathrm{id}$ and $f_#z$ bounds, then $z$ bounds. Separately, elementwise Mayer–Vietoris injectivity at $H_1$ says that if $U\cup V=X$ are open, $H_2(X)=0$, and a $1$-cycle of $U\cap V$ pushes forward to boundaries in $U$ and in $V$, then it already bounds in the intersection.
Here the geometric cover is by two closed halves of a union; the algebraic work is to reduce that cover, via homeomorphisms of complements, to the open MV setting of the midpoint complement $(K_P\cap K_M)^c$.
proof idea
Substitute $K_U=K_P\cup K_M$. On the midpoint space $(K_P\cap K_M)^c$, the sets ${x\notin K_P}$ and ${x\notin K_M}$ are open and cover the whole space. Transport $z$ across the union-complement homeomorphism $e$ to a cycle $z'$ (using that chain maps send cycles to cycles).
On each half, compose with a flatten-complement homeomorphism and apply the retraction lemma so that the given bounding hypotheses on the original half-complements become bounding hypotheses for the MV inclusions of $z'$. Invoke elementwise MV injectivity (with the $H_2=0$ hypothesis) to conclude $z'$ bounds in the midpoint. Pull the bound back along $e$ by the retraction lemma again.
why it matters
This is the algebraic engine of geometric bisection on an embedded arc. Downstream, bad_step uses it to show that a bad parameter interval (one whose arc-image complement still carries a nonbounding cycle) has a bad half of half the length, enabling infinite descent.
In the broader Recognition foundation, arc-complement acyclicity feeds the linking analysis that forces spatial dimension $D=3$ (T8/T9 in the forcing chain). Without a clean bisection step, one cannot run the nested-interval argument that kills nontrivial $H_1$ of the full arc complement. The result is fully proved (no sorry); it closes the MV half of that descent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.