bad_step
plain-language theorem explainer
A bad parameter interval for an embedded arc on the 3-sphere always has a bad half of half the length. Anyone building the nested bisection sequence that forces a linking contradiction cites this step. The proof splits at the midpoint and, if both halves bound, feeds the two-arc Mayer–Vietoris lemma with vanishing H₂ of a punctured sphere.
Claim. Let $a$ be an injective continuous path into the $D$-sphere ($D=3$) and let $z$ be a $1$-cycle in the complement of the image of $a$ that is a boundary-free cycle on the full complement. If $[u,v]\subseteq[0,1]$ is bad for $(a,z)$ (the pushforward of $z$ into the complement of $a([u,v])$ is not a boundary), then there exists a subinterval $[q_1,q_2]\subseteq[u,v]$ of length $(v-u)/2$ that is likewise bad.
background
The module develops acyclicity of arc complements in the $D$-sphere with $D=3$ forced by the linking requirement (T8/T9 in the forcing chain). An arc $a$ is a continuous injective map from the unit interval into $\mathrm{Sph},D$. For parameters $u\le v$ the set $\mathrm{seg}(a,u,v)$ is the image $a([u,v])$; it is closed because it is compact in a Hausdorff space.
The predicate $\mathrm{Bad}(a,z,u,v)$ packages the bisection invariant: $[u,v]\subseteq[0,1]$ and the restricted cycle $z\mathrm{Seg}(a,z,u,v)$ is not a boundary in the complement of that segment. The ambient hypothesis is that $z$ itself is a cycle (boundary zero) in the complement of the full image of $a$.
Upstream, bounds_of_halves is the elementwise two-arc Mayer–Vietoris step: a $1$-cycle of the complement of $K_U=K_P\cup K_M$ whose pushforwards bound in both half-complements already bounds, once $H_2((K_P\cap K_M)^c)=0$. Intersection of adjacent segments collapses to a singleton by injectivity of $a$, and the complement of a point in $S^3$ is contractible, so that $H_2$ vanishes.
proof idea
Unpack the Bad hypothesis to get $0\le u\le v\le 1$ and non-bounding of the full segment cycle. Set the midpoint $m=(u+v)/2$. Case-split on whether $[u,m]$ is Bad.
If yes, return $(u,m)$ with the length identity by ring. If not, the left half bounds; claim the right half $[m,v]$ is Bad. Suppose toward contradiction it also bounds. Then both halves bound. By seg_inter and injectivity the two segments meet at the single point $a(m)$. The complement of that point is contractible, so $H_2$ of the intersection-complement is zero. Feed closedness of both segments, their union identity, the cycle hypothesis, and the two restricted bounding witnesses into bounds_of_halves. The conclusion is that the full-segment cycle bounds, contradicting Bad on $[u,v]$.
why it matters
This is the inductive engine of the nested bad-interval construction. Downstream, badSeq builds a sequence of nested Bad pairs by repeatedly choosing the witness of bad_step, and badSeq_succ records the nesting and exact halving of lengths. The resulting Cauchy nest collapses to a point of the arc whose removal still leaves a non-bounding cycle, contradicting contractibility of the punctured $3$-sphere.
In the Recognition framework the argument sits inside the foundation layer that forces $D=3$ spatial dimensions (primer T8; the constant $D$ is defined as $3$ because linking requires it). Acyclicity of arc complements is the topological half of the linking-vanishing package imported from LinkingVanishingHighDim, which underwrites the dimensional forcing used throughout the monolith. The lemma itself is fully proved; it closes no sorry, but it is the step that makes the infinite bisection well-defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.