badSeq_succ
plain-language theorem explainer
Successive terms of the nested bad-interval sequence have nondecreasing left endpoint, nonincreasing right endpoint, and halved width. Monotonicity, antitonicity, and exact-width lemmas cite this step. The proof unpacks the choice specification of the bisection lemma on the current term's Bad invariant.
Claim. For every $k\in\mathbb{N}$, if $(u_k,v_k)$ is the $k$-th term of the nested bad-interval sequence (built from an injective arc $a$, a $0$-boundary class $z$, and an initial Bad interval on $[0,1]$), then $u_k\le u_{k+1}$, $v_{k+1}\le v_k$, and $v_{k+1}-u_{k+1}=(v_k-u_k)/2$.
background
The module develops an arc-complement acyclicity argument in the sphere: an injective continuous arc $a$ and a singular class $z$ that is a boundary on the complement are used to build nested real intervals that remain "bad" (the Bad predicate packages endpoint bounds, positive length, and a non-bounding obstruction for $z$).
The recursive sequence badSeq starts from a Bad interval on $[0,1]$ and at each step applies the bisection lemma: every Bad interval has a Bad half of half the length. The sequence values are dependent pairs carrying both the endpoint pair and a proof of Bad.
Upstream, bad_step states exactly the existence claim used here: given Bad on $(u,v)$, there is a subinterval $(q_1,q_2)$ still Bad with $u\le q_1$, $q_2\le v$, and $q_2-q_1=(v-u)/2$.
proof idea
Term-mode unpacking of the bisection choice. Apply bad_step to the Bad witness stored in the $k$-th sequence term, take choose_spec of the resulting existential, and project the three conjuncts (left inequality, right inequality, halved length). No induction and no extra arithmetic.
why it matters
This is the one-step interface between the bisection lemma and the global nested-interval calculus. Downstream, badSeq_mono and badSeq_anti are the monotone/antitone packages obtained by feeding the two endpoint inequalities into the standard Nat-of-succ lemmas; badSeq_width inducts on the halved-length identity to get width exactly $2^{-k}$.
Those three facts drive the nested-interval limit that forces a contradiction with the Bad obstruction, closing the arc-complement acyclicity argument in this foundation module (high-dimensional linking/vanishing context imported from LinkingVanishingHighDim). It is pure topological scaffolding for the RS forcing chain's geometric side, not a constants or mass-ladder claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.