badSeq_props
plain-language theorem explainer
For each index of the nested bad-interval sequence used in the arc-complement argument, the left endpoint is nonnegative, the right endpoint is at most one, and the pair is ordered. Anyone running the bisection construction for H₁-acyclicity of arc complements in S^D cites this. The proof is a three-projection term from the Bad subtype witness already stored on the sequence.
Claim. Let $(u_k,v_k)$ be the $k$-th pair in the nested bad-interval sequence associated to an injective arc $a$ and a reference $1$-cycle $z$ that is nonbounding on the full complement. Then $0\le u_k$, $v_k\le 1$, and $u_k\le v_k$.
background
The ambient theorem is arc-complement acyclicity (Hatcher 2B.1, arc case): every topological embedding of the unit interval into the $D$-sphere has $H_1$-acyclic complement. The proof strategy is nested bisection of a "bad" interval on which a fixed reference cycle remains nonbounding in the complement of the image arc segment.
Bad(u,v) is the bisection invariant: $[u,v]\subseteq[0,1]$ with $u\le v$, and the pushforward of the reference cycle into the complement of $a([u,v])$ is not a boundary. The nested sequence badSeq is defined by recursion, starting from the full interval $[0,1]$ (assumed bad) and at each step choosing a half that remains bad; each term is a subtype pair carrying a proof of Bad.
Spatial dimension $D$ is the RS-forced value $3$ (T8/T9), though the formal statement is written for general $D$.
proof idea
One-line term proof. The value badSeq ... k is a subtype element whose second component is a proof of Bad on the stored endpoints. Bad is the four-way conjunction $0\le u\land v\le 1\land u\le v\land\neg(\text{boundary})$. The proof projects the first three conjuncts via nested .2 accessors and packages them as an And triple. No lemmas are applied.
why it matters
This is a local bookkeeping lemma inside the formalization of arc-complement acyclicity (module doc: Hatcher 2B.1, arc case, every embedding $I\hookrightarrow S^D$ has $H_1$-acyclic complement). The nested bad sequence is the engine of the bisection: without named access to $0\le u_k\le v_k\le 1$, later steps cannot invoke interval arithmetic, midpoint selection, or the diameter-to-zero argument that produces a point of the arc whose removal still leaves a nonbounding cycle.
No downstream consumers are recorded yet (used_by empty), so the lemma is presently an internal extraction used by later material in the same Geometry section before the main theorem. In the broader RS foundation it supports the topological half of the linking/dimension story that forces $D=3$ (T8), though this particular projection is dimension-agnostic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.