singularTwoBoundaryFree_freeMk_linearSingularTwoSimplex
plain-language theorem explainer
Geodesic composition law on free singular chains of the circle: the free boundary of the lift-affine 2-simplex on real lifts (p,q,r) equals geo(q,r) − geo(p,r) + geo(p,q). Anyone showing that geodesics compose additively in H₁(S¹) cites this identity. The proof unfolds the linear 2-simplex and rewrites against the three face-map lemmas.
Claim. For all real lifts $p,q,r$, the free singular boundary of the lift-affine singular $2$-simplex with vertices $(p,q,r)$ equals the free $1$-chain $\mathrm{geo}(q,r)-\mathrm{geo}(p,r)+\mathrm{geo}(p,q)$, where $\mathrm{geo}(a,b)$ is the geodesic singular $1$-simplex obtained by projecting the straight line from $a$ to $b$ in the universal cover $\mathbb{R}\to S^1$.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$ and proves that the invariant kills boundaries, so it descends to homology. The key scalar is simplex displacement: reparameterize a singular $1$-simplex $\Delta^1\to S^1$ to the unit interval and take path displacement (equal to $2\pi$ times winding).
A geodesic singular $1$-simplex $\mathrm{geo}(a,b)$ is the projection of the straight-line path in the cover from lift value $a$ to $b$. The lift-affine $2$-simplex on $(p,q,r)$ is the continuous map $\Delta^2\to S^1$ whose lift is affine on the three vertex lifts; its singular version is the free generator fed to the free boundary map.
Upstream face lemmas identify the three faces: $\delta_0$ is $\mathrm{geo}(q,r)$, $\delta_1$ is $\mathrm{geo}(p,r)$, and $\delta_2$ is $\mathrm{geo}(p,q)$. The module goal is the chain-level half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding is a left inverse to the fundamental class.
proof idea
Short rewrite proof. Unfold the definition of the lift-affine singular $2$-simplex as the singular simplex of the linear $2$-simplex map. Apply the free-boundary evaluation lemma that turns free generators into alternating face sums. Rewrite the three face terms via the singular-simplex face formula, then replace each face by the corresponding geodesic using the three face identities: face $0$ is $\mathrm{geo}(q,r)$, face $1$ is $\mathrm{geo}(p,r)$, face $2$ is $\mathrm{geo}(p,q)$. The alternating sum is then exactly the claimed free chain.
why it matters
This is the geodesic composition law at free-chain level: $\mathrm{geo}(p,q)+\mathrm{geo}(q,r)$ is homologous to $\mathrm{geo}(p,r)$ in free $C_1$. Downstream it is restated as the free-chain form used throughout the winding-chain development (boundary of the lift-affine $2$-simplex equals $\mathrm{geo}(q,r)-\mathrm{geo}(p,r)+\mathrm{geo}(p,q)$).
Together with the kills-boundaries identity for arbitrary singular $2$-simplices and the fact that the once-around generator has winding $1$, it supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module notes the converse generation half still needs a simplicial prism/subdivision operator not yet in Mathlib singular homology. In the Recognition foundation stack this pins the integer winding comparison that later feeds circle-based forcing and octave bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.