range_subset_seg
plain-language theorem explainer
The image of an arc a : I → S^D sits inside the parameter segment of a from 0 to 1. Used by anyone assembling arc-complement acyclicity on the sphere. Proof is a direct unpacking of the unit-interval subtype bounds.
Claim. If $a$ is an arc from the unit interval into the $D$-sphere, then $\mathrm{range}(a) \subseteq \mathrm{seg}(a;0,1)$, where $\mathrm{seg}(a;u,v)$ is the image under $a$ of the parameter set $\{q \in I : u \le q \le v\}$.
background
The module develops arc-complement acyclicity on spheres: every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement (Hatcher 2B.1, arc case). An arc $a$ is such an embedding $I \hookrightarrow S^D$.
The auxiliary set $\mathrm{seg}(a;u,v)$ is the image of the closed parameter subinterval $[u,v]\cap I$ under $a$. In particular $\mathrm{seg}(a;0,1)$ is the image of the full unit interval, so the claimed containment is the elementary observation that every parameter already lies in $[0,1]$.
The surrounding development imports linking-vanishing machinery in high dimensions and works throughout with the sphere as a $T_2$ space.
proof idea
Term proof by set introduction. A point of the range is $a(q)$ for some $q\in I$. The subtype bounds on $q$ give $0\le q\le 1$, so $q$ belongs to the defining parameter set of $\mathrm{seg}(a;0,1)$, and $a(q)$ is therefore in that image. No external lemmas are required.
why it matters
Supplies the full-parameter containment used inside arcComplementsAcyclic, the formal Hatcher 2B.1 statement that every arc embedding into $S^D$ has $H_1$-acyclic complement in every dimension $D$. That theorem is the arc case of the linking-vanishing package imported from LinkingVanishingHighDim.
In the Recognition Science foundation layer this topological fact underwrites high-dimensional linking arguments that feed the forcing chain (spatial dimension $D=3$ at T8, eight-tick structure). The lemma itself is purely set-theoretic bookkeeping; its value is that the parent acyclicity theorem can quote a named containment rather than inline the subtype unpacking.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.