seg_inter
plain-language theorem explainer
Contiguous parameter segments of an injective arc on the D-sphere meet only at the shared endpoint: the image of [u,m] intersects the image of [m,v] in exactly {a(m)}. Cited by the bisection step that halves bad intervals in the arc-complement acyclicity argument. Proof is a short set-image calculation: injectivity pulls intersection inside, then order antisymmetry pins the parameter set to a singleton.
Claim. Let $a$ be an injective map from the unit interval into the $D$-sphere ($D=3$). For real parameters with $0\le m\le 1$, $u\le m$, and $m\le v$, the arc-segment images satisfy $\mathrm{seg}(a,u,m)\cap\mathrm{seg}(a,m,v)=\{a(m)\}$.
background
The ambient space is the $D$-sphere with $D=3$, the spatial dimension forced by the Recognition forcing chain (T8/T9). An arc $a$ is a map from the unit interval into that sphere; the local object of study is its complement in the sphere, whose singular homology is being controlled.
The helper seg is the image under $a$ of a closed parameter subinterval: $\mathrm{seg}(a,u,v)=a\bigl({q\in I:u\le q\le v}\bigr)\subseteq S^D$. Contiguous segments $\mathrm{seg}(a,u,m)$ and $\mathrm{seg}(a,m,v)$ therefore share the candidate point $a(m)$, and the question is whether injectivity of $a$ forces that point to be the entire intersection.
The module sits in the Foundation layer that feeds linking-vanishing statements in high dimension: acyclicity of arc complements is the geometric input those vanishing results need.
proof idea
Unfold the definition of seg so both sides are images under $a$. Injectivity of $a$ rewrites the intersection of images as the image of the intersection of the two parameter sets. The parameter intersection is shown by ext and simp to be the singleton ${m}$: the forward direction uses le_antisymm on the two inequalities $q\le m$ and $m\le q$; the reverse plugs in $m$ with le_refl and the given bounds $u\le m\le v$. Finally Set.image_singleton yields ${a(m)}$.
why it matters
Feeds the bisection lemma bad_step ("a bad interval has a bad half"), which is the inductive engine of the arc-complement acyclicity argument in this module. Without a clean singleton intersection at the midpoint, the homology class supported on a bad parameter interval could not be pushed onto a strictly shorter half while staying in the complement of the remaining arc.
In the broader Recognition framework this is geometric scaffolding for linking vanishing on $S^D$ with $D=3$ (the dimension forced by T8). Acyclicity of arc complements is the reason one-dimensional cycles in the complement bound, which in turn supports the high-dimensional linking statements imported from LinkingVanishingHighDim. No open scaffold remains here: the lemma is fully proved and only used as a local set-identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.