seg_mono
plain-language theorem explainer
If the parameter window shrinks inside a larger one, the corresponding arc image on the sphere is nested. Anyone running the bisection argument on bad intervals cites this set inclusion. The proof is a direct membership chase through the image definition of the segment.
Claim. Let $a$ be an arc into the sphere. For real parameters $u' \le u \le v \le v'$, the image of the parameter set $\{q \in [0,1] : u \le q \le v\}$ under $a$ is contained in the image of $\{q \in [0,1] : u' \le q \le v'\}$.
background
The ambient module studies acyclicity of the complement of an arc in the sphere $S^D$. An arc $a$ is a continuous path into the sphere; the local object of interest is the image of a closed parameter subinterval under that path.
The definition seg packages that image: for reals $u,v$, it is $a''{q \in [0,1] : u \le q \le v}$, a subset of the sphere. Nested parameter windows therefore induce nested images, which is the content of the present lemma.
This sits inside the bisection machinery used to control homology classes supported off the arc. The downstream step bad_step repeatedly halves a "bad" parameter interval while preserving a nonvanishing boundary condition on the complement.
proof idea
Unfold set membership in the image. A point of seg a u v is $a(q)$ for some $q \in [0,1]$ with $u \le q \le v$. The hypotheses $u' \le u$ and $v \le v'$ give $u' \le q \le v'$ by transitivity of $\le$, so the same $q$ witnesses membership in seg a u' v'. No external lemmas are required beyond the definition of seg.
why it matters
The lemma is a bookkeeping inclusion for the bisection argument. Downstream, bad_step asserts that every bad parameter interval has a bad half of half the length; nesting of segments lets the badness predicate pass from a parent interval to a child without enlarging the geometric support on the sphere.
In the broader ArcComplementAcyclic development this supports vanishing of low-dimensional linking/homology data off an embedded arc, a foundation fact used when the Recognition forcing chain needs topological control in dimension $D$ (cf. the $D=3$ landmark T8 and the eight-tick discrete structure). It does not itself force constants or the J-cost; it is pure set-theoretic support for the acyclicity argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.