seg_union
plain-language theorem explainer
For an arc on the sphere, the image of a closed parameter interval equals the union of the images of its two contiguous subintervals when the cut lies between the endpoints. Bisection lemmas in the arc-complement acyclicity argument cite this set identity. The proof unfolds the image definition, rewrites via image-union, and splits on the total order of the reals.
Claim. Let $a$ be an arc into the sphere and let $u,m,v\in\mathbb{R}$ satisfy $u\le m\le v$. Then the image of the parameter set $\{q\in I:\,u\le q\le v\}$ under $a$ equals the union of the images of $\{q\in I:\,u\le q\le m\}$ and $\{q\in I:\,m\le q\le v\}$.
background
The module develops acyclicity of the complement of an embedded arc in the sphere $S^D$, in the style of classical linking and Alexander duality arguments used in the Recognition foundation layer.
The local object is seg: for an arc $a$ and reals $u,v$, it is the image $a''{q\in I:u\le q\le v}$, i.e. the portion of the arc whose parameter lies in the closed interval between $u$ and $v$. Intervals here are cut inside the unit interval $I$, then pushed forward by $a$ into the sphere.
Totality of the real order ($x\le y$ or $y\le x$) is the only nontrivial comparison fact used when a parameter is tested against the cut point $m$.
proof idea
Unfold the definition of the arc segment as an image of a parameter set. Rewrite the goal with the standard identity that the image of a union is the union of images, then reduce to equality of the two parameter sets by congruence and extensionality.
For membership of a parameter $q$: if $u\le q\le v$, split on whether $q\le m$ or $m\le q$ (totality of $\le$ on $\mathbb{R}$) to land in the left or right half. Conversely, each half membership extends to the full interval by transitivity with the hypotheses $u\le m$ and $m\le v$.
why it matters
The lemma is the set-theoretic glue for the bisection step bad_step: a bad parameter interval has a bad half of half the length. That step is the inductive engine in the arc-complement acyclicity development (module ArcComplementAcyclic), which supports high-dimensional linking-vanishing arguments imported from LinkingVanishingHighDim.
In the Recognition forcing chain this sits in the topological foundation layer that underwrites dimension and connectivity constraints (T8 forces $D=3$ spatial dimensions; eight-tick and sphere topology sit nearby). It does not itself mention $J$, $\varphi$, or the RCL; it is pure interval arithmetic on arc images, needed so later homology vanishing can run a nested-interval argument without gaps at cut points.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.