zSeg_restrict
plain-language theorem explainer
If a parameter subinterval maps into a larger one under the arc, the degree-1 chain map of the complement inclusion carries the pushforward reference cycle on the larger complement to that on the smaller. Used by the bisection step that halves bad intervals. Proof is an unfold plus chain-map functoriality and inclusion composition.
Claim. Let $a$ be an arc in the sphere and $z$ a reference $1$-cycle. Write $\mathrm{seg}(u,v)$ for the image $a([u,v])$. If $\mathrm{seg}(u',v')\subseteq\mathrm{seg}(u,v)$, then the degree-$1$ chain map induced by the continuous inclusion of complements $\{y\notin\mathrm{seg}(u,v)\}\hookrightarrow\{y\notin\mathrm{seg}(u',v')\}$ sends the pushforward of $z$ into the larger complement to the pushforward of $z$ into the smaller complement.
background
The module works in singular chain complexes of open complements of arc images on the sphere $\mathrm{Sph},D$. For real parameters $u\le v$, $\mathrm{seg}(u,v)$ is the image of the closed parameter interval under the arc $a$. The complement inclusion $cInc$ is the continuous map from the complement of a larger set into the complement of a smaller set whenever the sets are nested.
The object $zSeg(u,v)$ is the image of a fixed reference $1$-cycle $z$ under the chain map of the inclusion of the full arc-complement into the complement of $\mathrm{seg}(u,v)$. In other words it is the pushforward of $z$ living in $C_1$ of that smaller open set. Functoriality of the singular chain functor supplies an elementwise identity $\mathrm{chainMap},g\circ\mathrm{chainMap},f=\mathrm{chainMap}(f\gg g)$, and the inclusions compose strictly: $cInc(h_1)\gg cInc(h_2)=cInc(h_2\circ h_1)$.
The local goal is a bisection invariant: an interval is "bad" when the pushforward cycle is not a boundary. Nested restriction of that cycle is the algebraic step needed before one can split a bad interval in half.
proof idea
Term-mode, three steps. Unfold the definition of the pushforward cycle on both sides; each side becomes a composite chain map applied to the reference cycle $z$. Rewrite the left-hand composite by the elementwise functoriality lemma for chain maps, replacing the two successive chain maps by the chain map of the composite continuous map. The composite of the two complement inclusions is definitionally the single inclusion for the transitive nesting $\mathrm{seg}(u',v')\subseteq\mathrm{seg}(u,v)$ (by the composition law for $cInc$), so both sides match.
why it matters
Feeds the bisection lemma bad_step: a bad parameter interval has a bad half of half the length. That step is the inductive engine for showing that if the full-arc pushforward is nonbounding, then arbitrarily fine nested subarcs remain nonbounding, which is the obstruction half of the arc-complement acyclicity argument in this foundation module.
The surrounding development sits under high-dimensional linking and vanishing (imported from LinkingVanishingHighDim) and uses the hand-proved infinite-order property of the once-around loop on the circle. Within Recognition Science this is pure topological scaffolding for the forcing chain's geometric side (dimension and octave structure), not a direct citation of T5–T8 or the J-cost equation. It closes no open generation question; it only moves cycles under nested inclusions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.