cVal_injective
plain-language theorem explainer
The continuous inclusion of a set-complement subtype into the ambient topological space is injective on underlying points. Anyone building chain maps or homology arguments for arc complements in spheres cites this. The proof is a one-line application of subtype extensionality to equal underlying values.
Claim. For any subset $S$ of the ambient space $W$, the continuous inclusion map $\{y \in W : y \notin S\} \to W$ is injective on points.
background
In the arc-complement setting one works with an ambient space $W$ (typically a sphere $S^D$ or a related TopCat object) and a closed set $S \subseteq W$. The complement is packaged as the subtype ${y : W \mid y \notin S}$, equipped with the subspace topology.
The morphism cVal S is exactly the continuous inclusion of that subtype into $W$: its underlying map is Subtype.val. Homology and linking arguments later treat this inclusion as a chain-level map, so injectivity of the point-set map is the first algebraic fact needed.
The parent development formalizes Hatcher's arc-complement acyclicity: every topological embedding of the unit interval into $S^D$ has $H_1$-acyclic complement in every dimension $D$.
proof idea
Term-mode one-liner. Given two elements of the complement subtype whose images under the underlying map of cVal S agree, apply Subtype.ext to conclude the subtype elements are equal. No continuity or topology is used beyond the definition of the inclusion.
why it matters
Feeds directly into arcComplementsAcyclic, the formal statement of Hatcher's theorem 2B.1 (arc case): every embedded arc in $S^D$ has $H_1$-acyclic complement. Injectivity of the complement inclusion is the elementary set-theoretic step before chain maps, cycle classes, and vanishing of $H_1$ are assembled.
In the Recognition Science foundation layer this sits inside the topological scaffolding that supports dimension and linking arguments (related to the forcing chain's $D = 3$ step and high-dimensional vanishing results imported from LinkingVanishingHighDim). It is pure topology, not a physics identity, but it is load-bearing for the acyclicity theorem the module exists to prove.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.