simplexDisplacement_boundary
plain-language theorem explainer
For every continuous map F from the standard 2-simplex into S¹, the alternating sum of path displacements on the three faces vanishes. Algebraic topologists and anyone building the winding homomorphism on singular 1-cycles cite this as the chain-level “kills boundaries” identity. The proof pushes a rel-endpoint homotopy in the simply connected Δ² through F, then applies additivity and homotopy invariance of path displacement.
Claim. Let $F:\Delta^2\to S^1$ be continuous. Write $\delta_i F$ for the $i$-th face (a singular $1$-simplex). Then $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$, where $\mathrm{disp}$ is the real displacement of the path obtained by reparameterizing $\Delta^1$ to the unit interval.
background
This module lifts the path-level displacement of CircleWinding to singular simplices of $S^1$. A singular $2$-simplex is a continuous map $F:\Delta^2\to S^1$ with $\Delta^2=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},3)$. Displacement of a path $\gamma:I\to S^1$ is the net travel of its canonical real lift: $\mathrm{pathDisplacement}(\gamma)=\Gamma(1)-\Gamma(0)$. On a singular $1$-simplex one reparameterizes $\Delta^1$ to $I$ and takes that number.
The standard simplex is convex, hence simply connected (stdSimplex_simplyConnectedSpace). Homotopy invariance of displacement says that paths homotopic rel endpoints have equal displacement; additivity says displacement of a concatenated path is the sum of the pieces. Those two facts, plus the covering lift of the trigonometric map $\mathbb{R}\to S^1$, are the only analytic input.
The module goal is the single identity that makes displacement a homology invariant: alternating face sums on every $2$-simplex vanish, so the functional descends to $1$-cycles.
proof idea
Instantiate simple connectedness of $\Delta^2$. The broken edge walk $v_0\to v_1\to v_2$ is therefore path-homotopic rel endpoints to the direct edge $v_0\to v_2$. Push the homotopy forward along $F$ and rewrite the image of the concatenation via Path.map_trans, obtaining a rel-${0,1}$ homotopy of continuous maps $I\to S^1$.
Homotopy invariance (pathDisplacement_homotopic) plus additivity (pathDisplacement_trans) give a telescoping equality: displacement of the direct edge equals the sum of the two broken edges. Identify each face displacement with the corresponding edge displacement via the face-edge comparison lemmas, substitute, and cancel with ring.
why it matters
This is the chain-level “winding kills boundaries” step advertised in the module doc. Downstream, simplexWinding_boundary rescales by $2\pi$ to obtain the same identity for integer winding numbers. Together with the fact that the once-around generator has winding $1$, one obtains a homomorphism on $1$-cycles that is a left inverse to the fundamental class: the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
In the Recognition Science foundation stack this supplies the topological half of the circle’s first homology, used wherever the eight-tick octave and phase/winding bookkeeping need a rigorously vanishing boundary contribution. The converse generation statement (every $1$-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism or subdivision operator that Mathlib’s singular homology does not yet provide; this theorem closes only the kills-boundaries half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.