seg
plain-language theorem explainer
Defines the closed arc segment obtained by pushing a parameter subinterval [u, v] forward under a continuous path a into the D-sphere. Algebraic topologists cite it when running the bisection argument for H₁-acyclicity of arc complements (Hatcher 2B.1). The body is a direct image of a closed subset of the unit interval under the underlying map of a.
Claim. For real parameters $u,v$ and a continuous path $a$ into the $D$-sphere $S^D$, write $\mathrm{seg}(u,v)$ for the image $a\bigl(\{q\in[0,1]: u\le q\le v\}\bigr)\subseteq S^D$.
background
The ambient space is the topological $D$-sphere $\mathrm{Sph},D$, the unit sphere in Euclidean space of dimension $D+1$. Across the foundation modules, $D$ is fixed at $3$ by the forcing chain (T8 spatial dimensions; linking arguments also force $D=3$).
The module studies continuous embeddings $a:[0,1]\to S^D$ (arcs). The object here is the closed subarc cut out by restricting the parameter to a real interval $[u,v]$ and taking the image under $a$. Downstream lemmas treat these images as compact closed subsets of $S^D$, so their complements remain open subspaces on which singular chains and boundaries are well-defined.
This sits inside the arc-complement acyclicity development: one shows $H_1(S^D\setminus a([0,1]))=0$ by a nested-interval argument that repeatedly bisects parameter intervals whose pushforward cycles refuse to bound.
proof idea
Pure definition: the set-theoretic image of the preimage ${q\in I:u\le q\le v}$ under the underlying continuous map of $a$. No lemmas are applied; noncomputability is inherited from the sphere and path data.
why it matters
Local workhorse for the formal Hatcher 2B.1 arc case. Parent results include arcComplementsAcyclic (every embedded arc in $S^D$ has $H_1$-acyclic complement), the bisection invariant Bad (a parameter interval whose pushed cycle is not a boundary in the complement of the corresponding segment), and bad_step (every bad interval has a bad half of half the length).
Supporting topology lemmas (isCompact_seg, isClosed_seg, range_subset_seg, monotonicity and intersection facts) all quote this image. In the Recognition framework the result feeds the high-dimensional linking-vanishing story that underwrites $D=3$ (T8/T9): once arc complements are $H_1$-acyclic, linking obstructions force three spatial dimensions rather than a free choice of $D$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.