cInc_comp_cVal
plain-language theorem explainer
If S ⊆ T in the ambient space W, the inclusion of the complement of T into the complement of S, composed with the inclusion of that larger complement into W, equals the direct inclusion of the complement of T into W. Arc-complement and linking arguments cite this as the basic naturality of complement inclusions. The proof is definitional: extensionality on points, then rfl.
Claim. Let $W$ be the ambient topological space and $S \subseteq T \subseteq W$. Write $c_{\mathrm{inc}}(S\subseteq T): W\setminus T \to W\setminus S$ for the continuous inclusion of complements induced by $S\subseteq T$, and $c_{\mathrm{val}}(U): W\setminus U \to W$ for the subtype inclusion of a complement. Then $c_{\mathrm{val}}(S)\circ c_{\mathrm{inc}}(S\subseteq T) = c_{\mathrm{val}}(T)$ as morphisms in $\mathbf{Top}$.
background
The module develops arc-complement acyclicity in the style of Hatcher 2B.1: every topological embedding of the unit interval into a sphere has $H_1$-acyclic complement. Complements are handled as subtypes of an ambient space $W$, packaged as objects of TopCat.
Two maps are fixed. For $S\subseteq T$, the morphism $c_{\mathrm{inc}}$ is the continuous inclusion of the complement of the larger set into the complement of the smaller set (so $W\setminus T\hookrightarrow W\setminus S$). Independently, $c_{\mathrm{val}}(S)$ is the continuous subtype projection $W\setminus S\hookrightarrow W$. Both are built with TopCat.ofHom from the obvious set-theoretic maps and continuity of subtype valuation.
This lemma records that those two constructions commute with composition: going through the intermediate complement $W\setminus S$ is the same as including $W\setminus T$ directly into $W$. It is the elementary naturality square for complement inclusions used throughout the acyclicity argument.
proof idea
Term-mode proof by pointwise extensionality on the underlying continuous map. After ext x, both sides send a point of the complement of $T$ to its underlying point in $W$, so the equality is definitional (rfl). No auxiliary lemmas are required; the result is immediate from the definitions of $c_{\mathrm{inc}}$ and $c_{\mathrm{val}}$.
why it matters
Feeds the main theorem arcComplementsAcyclic: every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement, in every dimension $D$ (Hatcher 2B.1, arc case, formal). That theorem works by contradiction on nonvanishing $H_1$ of the complement and needs a coherent family of maps between complements as the arc (or its approximating sets) varies; this composition identity keeps those maps consistent with the ambient inclusions.
In the Recognition foundation stack the result is pure topology scaffolding for linking and vanishing statements imported from LinkingVanishingHighDim. It does not itself encode a forcing-chain step (T0–T8), the Recognition Composition Law, or a physical constant; it is infrastructure so that arc-complement homology can be stated cleanly in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.