badSeq_mono
plain-language theorem explainer
The left endpoints of the nested bad-interval sequence are nondecreasing in the step index. Anyone running the nested-interval argument that forces a homology class in an arc complement to vanish will cite this comparison. The proof is a one-line wrapper: successive left-endpoint inequalities from the successor step, fed to the standard ℕ-monotonicity lemma.
Claim. Let $(\ell_k,r_k)_{k\in\mathbb{N}}$ be the nested bad-interval sequence attached to an injective arc $a$ and a homology class $z$ with vanishing boundary. Then $k\mapsto\ell_k$ is monotone: $\ell_k\le\ell_{k+1}$ for every $k$.
background
The ambient construction lives in the arc-complement acyclicity argument: an injective continuous arc $a$ in the $D$-sphere, and a singular homology class $z$ on the complement whose boundary vanishes. A pair of reals $(p,q)$ is called bad when the restricted class still obstructs acyclicity on the corresponding sub-arc data.
The nested sequence badSeq starts from a bad unit interval $(0,1)$ and iteratively applies a bisection step that returns a strictly nested bad subinterval of half the length, carrying the Bad invariant at every stage. The successor lemma records three comparisons at once: left endpoints nondecrease, right endpoints nonincrease, and length halves.
Monotonicity of the left-endpoint projection is the fragment needed before one can compare left endpoints at arbitrary indices against right endpoints at other indices.
proof idea
One-line term proof. Apply the library fact that a sequence on $\mathbb{N}$ is monotone once consecutive terms satisfy $x_k\le x_{k+1}$. The consecutive inequality is exactly the first conjunct of the successor lemma for the bad sequence, specialized at each $k$.
why it matters
Feeds the two-index comparison that any left endpoint is at most any right endpoint along the nested sequence. That comparison is the quantitative backbone of the nested-interval squeeze: lengths go to zero while the intervals stay bad, forcing the obstructing class to be zero and thereby proving the arc complement is acyclic in the relevant degree.
Within the Foundation layer this is bookkeeping inside the high-dimensional linking/vanishing pipeline (imported from LinkingVanishingHighDim), not a forcing-chain landmark itself. It closes no open scaffold; it is a proved monotone fragment used immediately by the next lemma in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.