badSeq
plain-language theorem explainer
Nested bisection sequence of bad parameter intervals for an arc in the D-sphere. From the full [0,1] interval, each step halves while preserving the invariant that the pushed reference cycle does not bound in the complement of the arc image over that subinterval. Anyone proving arc-complement H₁-acyclicity by infinite descent cites this construction. Built by recursion on the choice witness from the half-interval lemma.
Claim. Fix an injective continuous map $a$ from the unit interval into the $D$-sphere, a $0$-cycle $z$ that is a boundary in the complement of the full image of $a$, and a witness that $[0,1]$ is bad (the pushforward of $z$ into the complement of $a([0,1])$ is not a boundary). There is a sequence of pairs $(u_k,v_k)\in\mathbb{R}\times\mathbb{R}$ such that each $[u_k,v_k]$ is bad, $(u_0,v_0)=(0,1)$, and each successor is a bad half of the previous interval (nested, length halved).
background
The ambient space is the unit $D$-sphere $\mathrm{Sph},D$ in Euclidean space of dimension $D+1$, with $D=3$ forced by the Recognition forcing chain (T8). Singular chains use the boundary operator $\mathrm{bnd}$ out of degree $n+1$ on the coproduct presentation of the chain groups.
A parameter interval $[u,v]\subseteq[0,1]$ is bad when the pushforward of a fixed reference cycle $z$ into the complement of the arc segment $a([u,v])$ is not a boundary. That is the bisection invariant. The half-interval lemma states that every bad interval admits a bad half of half the length, under injectivity of $a$ and the hypothesis that $z$ bounds in the full arc complement.
This module develops the arc case of Hatcher 2B.1 (linking vanishing / arc-complement acyclicity) inside the Recognition foundation stack that imports the high-dimensional linking vanishing interface.
proof idea
Recursive definition on $\mathbb{N}$, not a tactic proof. Base case $k=0$ packages the given badness witness for $(0,1)$. Successor applies the half-interval lemma to the previous term's badness proof, then takes the classical choice of a bad half pair together with its badness certificate. The resulting dependent pair is typed as a real pair subtype carrying the bad invariant at every index.
why it matters
This sequence is the engine of the infinite nested-interval argument for arc-complement acyclicity: every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement, in every dimension $D$ (Hatcher 2B.1, arc case). Downstream lemmas extract monotonicity of left endpoints, antitonicity of right endpoints, nested comparison, width halving, and destructured endpoint bounds; the main theorem arcComplementsAcyclic runs the contradiction by feeding the nested bad sequence into a limiting point argument.
In the Recognition framework the result supports the linking-vanishing side of the $D=3$ forcing (T8) and the high-dimensional linking package used for the alpha and gap bridges. It closes the constructive half of the bisection descent rather than leaving a scaffolding hole.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.