badSeq_zero
plain-language theorem explainer
The nested bad-interval sequence begins at the closed unit interval endpoints (0,1). Anyone running the width-halving induction or the arc-complement acyclicity argument needs this base value. The equality is definitional: it unfolds the k=0 clause of the recursive sequence.
Claim. For the nested bad-interval sequence built from an injective arc $a$, a 1-cycle $z$ with vanishing boundary, and a witness that $(0,1)$ is a bad interval, the zeroth term is exactly the pair $(0,1)$.
background
The ambient setting is the formalization of Hatcher's arc-complement acyclicity: every topological embedding of the unit interval into the $D$-sphere has $H_1$-acyclic complement. The proof proceeds by contradiction, producing a nested sequence of "bad" real intervals on which a fixed singular 1-cycle remains nontrivial in the complement of the arc image.
The sequence badSeq packages each stage as a subtype pair $(p,q)$ together with a Bad witness that the restricted interval still supports a nonzero homology class. By construction its zeroth clause is the unit interval $(0,1)$ with the initial badness hypothesis h0.
This lemma simply records that initial value, so later inductions (especially on interval width) have a clean base case.
proof idea
One-line definitional reflexivity. Unfolding the $k=0$ clause of badSeq yields $\langle(0,1), h0\rangle$ by construction, so the first projection equals $(0,1)$ by rfl.
why it matters
Feeds the base case of badSeq_width, which proves that the $k$-th bad interval has length $2^{-k}$. That geometric shrinkage is the engine of the contradiction in arcComplementsAcyclic (Hatcher 2B.1, arc case): an infinite nested sequence of positive-length bad intervals with widths tending to zero cannot exist once the arc is compact and the cycle is singular. Without the explicit start at $(0,1)$, the induction on width has nothing to stand on. In the broader Recognition foundation stack this is pure algebraic-topology scaffolding for linking-vanishing statements used upstream of dimensional forcing, not a physics claim itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.