badSeq_width
plain-language theorem explainer
The k-th nested bad interval for an embedded arc and a nontrivial 1-cycle has real width exactly 2^{-k}. Arc-complement acyclicity arguments cite this to force the nested intervals to a point. The proof is induction on k: base width 1 from the zero case, and the successor lemma halves the width.
Claim. For every $k \in \mathbb{N}$, if $(L_k, R_k)$ is the $k$-th nested bad interval produced from an injective arc embedding $a$ and a 1-cycle $z$ with the stated boundary and Bad hypotheses, then $R_k - L_k = 2^{-k}$.
background
The module develops arc-complement acyclicity on the sphere $S^D$: every topological embedding of the unit interval has $H_1$-acyclic complement (Hatcher 2B.1, arc case). The argument proceeds by contradiction: a nontrivial class in the complement yields a nested sequence of real intervals on which a "Bad" obstruction persists.
badSeq builds that nested sequence. It starts at the unit interval $(0,1)$ and, at each step, chooses a half-width subinterval that still carries the Bad predicate relative to the arc $a$ and cycle $z$. The companion lemmas record the base pair and the successor nesting: left endpoints are nondecreasing, right endpoints nonincreasing, and the length is exactly halved.
This width lemma converts that recurrence into a closed form. The ambient setting is the LinkingVanishingHighDim infrastructure imported by the module; injectivity of the arc and vanishing of the boundary of $z$ are fixed parameters of the sequence.
proof idea
Induction on $k$.
Zero case: rewrite by badSeq_zero, so the pair is $(0,1)$; norm_num gives width $1 = 2^{0}$.
Successor case: the third conjunct of badSeq_succ rewrites the new width as half the previous width; the inductive hypothesis substitutes $2^{-k}$, and ring finishes $2^{-(k+1)}$.
why it matters
Feeds the main theorem arcComplementsAcyclic: every embedding of the unit interval into $S^D$ has $H_1$-acyclic complement, in every dimension $D$. That theorem is the formal arc case of Hatcher 2B.1 and sits in the Foundation layer that underwrites higher linking and vanishing results used elsewhere in the monolith.
The closed-form width is the quantitative engine of the contradiction: the nested Bad intervals shrink to a single real parameter, at which the obstruction cannot survive under the injectivity and boundary hypotheses. Without exact halving, one only gets a nested family, not a forced collapse to a point.
In the broader Recognition stack this is pure topological scaffolding (not a T0–T8 forcing step), but it is the concrete algebraic-topology input that later linking-vanishing and dimension arguments rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.