constSimplex_pointOf
plain-language theorem explainer
Constant singular 0-simplices recover every 0-simplex from its underlying point: the two maps are inverse. Algebraic topologists working the singular chain complex of a space cite this when identifying degree-0 generators with points. The proof is a one-line appeal to 0-simplex extensionality plus the already-proved right inverse.
Claim. For any topological space $X$ and any singular $0$-simplex $s$ of $X$, the constant $0$-simplex at the underlying point of $s$ equals $s$ itself. Equivalently, $s \mapsto \mathrm{pt}(s)$ and $x \mapsto \mathrm{const}_x$ are mutually inverse between points of $X$ and $\mathrm{Idx}(X,0)$.
background
In the singular set of a space $X$, the index type $\mathrm{Idx}(X,n)$ is the set of singular $n$-simplices (maps from the standard simplex into $X$). Degree $0$ is special: a $0$-simplex is determined by a single point of $X$.
The module defines $\mathrm{pt}(s)$ as evaluation of $s$ at the unique vertex $v_0$ of $\Delta^0$, and $\mathrm{const}_X(x)$ as the constant map $\Delta^0\to X$ at $x$. The companion identity $\mathrm{pt}(\mathrm{const}_X(x))=x$ is already available as a simp lemma. A separate extensionality lemma states that two $0$-simplices are equal once their underlying points agree, via injectivity of the simplex equivalence and the subsingleton property of $\Delta^0$.
Local setting is the singular-sphere / singular-homology foundation layer: free abelian chains on these indices, with boundary and augmentation used later for path-connectedness arguments.
proof idea
Term-mode one-liner. Apply $0$-simplex extensionality (idx0_ext), whose hypothesis asks equality of underlying points. Discharge that hypothesis by rewriting with the simp lemma $\mathrm{pt}(\mathrm{const}_X(x))=x$ at $x=\mathrm{pt}(s)$. No further case splits or induction.
why it matters
Closes the bijection between points of $X$ and singular $0$-simplices, so degree-$0$ generators may be written interchangeably as points or as constant simplices. The sole recorded consumer is exists_bnd_of_pathConnected: in a path-connected space every $0$-chain is homologous to its total augmentation times a fixed base-point constant simplex. That lemma is the standard bridge from path-connectedness to $H_0\cong\mathbb{Z}$, which the singular-sphere development needs before Mayer–Vietoris and sphere homology computations.
Within Recognition Science this sits in the Foundation singular-homology stack (imports include SingularPrism, SingularPair, SingularSubdivision, SingularMayerVietoris). It is pure algebraic topology scaffolding rather than a T0–T8 forcing step; it underwrites later topological invariants used by the monolith, not a direct physics constant claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.