badSeq_le
plain-language theorem explainer
For the nested bad-interval sequence in the arc-complement bisection argument, every left endpoint is at most every right endpoint, for any pair of indices. Anyone closing the nested-interval limit (single point, or a limiting arc whose complement still carries a non-boundary cycle) needs this cross-index comparison. The proof is a two-case split on the order of the indices, chaining left-endpoint monotonicity, right-endpoint antitonicity, and the built-in left ≤ right of each Bad interval.
Claim. Let $(u_n,v_n)_{n\in\mathbb{N}}$ be the nested sequence of bad intervals produced by successive bisection from a reference non-boundary $1$-cycle on the complement of an embedded arc in $S^D$. Then for all $j,k\in\mathbb{N}$, one has $u_j\le v_k$.
background
The ambient setting is the formal arc case of Hatcher's linking-vanishing fact: every topological embedding $a:[0,1]\hookrightarrow S^D$ has $H_1$-acyclic complement. The proof proceeds by contradiction. Starting from a nonzero homology class $z$ on the full arc complement, one builds a nested sequence of closed subintervals of $[0,1]$ on which the pushed cycle remains non-boundary in the complement of the image arc segment.
A pair $(u,v)$ is Bad when $0\le u\le v\le 1$ and the pushforward of $z$ into the complement of $a([u,v])$ is not a boundary. The sequence badSeq starts at $(0,1)$ (assumed Bad) and at each step chooses a half-interval that preserves the Bad invariant, via a bisection lemma. Left endpoints are monotone nondecreasing; right endpoints are antitone nonincreasing. Each individual interval already satisfies left ≤ right by the Bad conjunction.
The present comparison is the missing cross-term: left of step $j$ versus right of step $k$, with no relation assumed between $j$ and $k$.
proof idea
Case-split on le_total j k.
If $j\le k$, apply left-endpoint monotonicity to get $u_j\le u_k$, then chain the Bad inequality $u_k\le v_k$ at index $k$.
If $k\le j$, start from the Bad inequality $u_j\le v_j$ at index $j$, then apply right-endpoint antitonicity to get $v_j\le v_k$.
Both legs are pure trans of the already-proved mono/anti lemmas with the $u\le v$ conjunct stored in the Bad witness carried by the sequence.
why it matters
This lemma is a local arithmetic fact inside the nested-interval engine that powers arcComplementsAcyclic, the formal statement that every embedded arc in $S^D$ has $H_1$-acyclic complement (Hatcher 2B.1, arc case, all dimensions $D$). The parent theorem runs by contradiction: a nonzero class on the full complement seeds a Bad interval $[0,1]$, the bisection sequence shrinks diameters to zero, and the limiting point would force the class to become a boundary, contradicting the invariant. Cross-index left ≤ right is needed to keep the nested family coherent when diameters and endpoints are compared across different stages.
In the Recognition Science foundation stack this sits under the topological forcing material that supports dimension and linking constraints (the same circle of ideas that feeds T8, $D=3$). It is pure algebraic topology bookkeeping; no Recognition-cost or $\varphi$-ladder content appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.