SingularTwoSimplex

The module lifts path-level winding and displacement on the circle to singular simplices of $S^1$, then proves the chain-level identity that displacement kills boundaries. A singular $n$-simplex is a continuous map from the standard topological $n$-simplex into the space; here the space is the actual Mathlib circle TopCat.sphere 1, not a project-local stand-in.

TopCat.toSSet is the singular simplicial-set functor. Evaluating at op (SimplexCategory.mk 2) selects continuous maps $\Delta^2 \to S^1$. The sibling type of singular $1$-simplices is defined the same way in degree $1$. Displacement of a $1$-simplex is path displacement after reparameterizing $\Delta^1$ to the unit interval; the key theorem is that the alternating face sum of any $2$-simplex has vanishing displacement.

That vanishing is the "winding kills boundaries" step toward a left inverse of the fundamental class on $H_1(S^1;\mathbb{Z})$.

Pure definitional abbreviation: expand to the object of the singular simplicial set of the circle at the opposite of the $2$-simplex object in the simplex category. No lemmas, tactics, or proof obligations.

This type is the carrier for every geometric $2$-cell used in the winding chain. Downstream constructions include the free boundary map sending a $2$-simplex to the alternating sum of its three $1$-faces; constant, linear (lift-affine), path-backtrack, and cone $2$-simplices; and the theorem that a cone $2$-simplex over a closed edge with matching faces proves the corresponding closed $1$-cycle bounds.

Together with displacement vanishing on boundaries and the fact that the once-around loop has winding $1$, the setup supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Surjectivity still needs a prism or subdivision operator that Mathlib singular homology does not yet provide. No Recognition forcing-chain step (T0–T8) is settled here; the declaration is pure singular-homology scaffolding for the circle winding invariant.