geodesicFreeChain
plain-language theorem explainer
Packages the lift-linear geodesic edge from real endpoints a to b as a free singular 1-chain generator on S¹. Anyone citing free-coordinate winding, fundamental-cycle comparison, or geodesic step identities uses this object. Construction is a one-line free-module generator of the singular simplex of the geodesic map.
Claim. For $a,b\in\mathbb{R}$, write $\mathrm{geo}(a,b)$ for the free singular $1$-chain on $S^1$ generated by the geodesic edge whose universal-cover lift is the straight line from $a$ to $b$ (projected to $S^1$).
background
The module builds the winding invariant on singular $1$-simplices of $S^1$ and proves it kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Displacement of a singular edge is path displacement after reparameterizing $\Delta^1$ to $[0,1]$; the key identity is that the alternating face sum of any singular $2$-simplex has displacement zero.
A geodesic $1$-simplex is the continuous map $\Delta^1\to S^1$ obtained by projecting the affine path $t\mapsto(1-t)a+tb$ in the cover $\mathbb{R}\to S^1$. The free $C_1$ is the free $\mathbb{Z}$-module on actual singular $1$-simplices of $\mathrm{TopCat.sphere},1$. Concrete continuous maps are turned into those simplices by the standard singular-set equivalence.
This definition is the free-module generator of that geodesic edge: the basic building block for free-coordinate statements about fundamental cycles, $2\pi\mathbb{Z}$ shifts, and composition of geodesic segments.
proof idea
Pure definitional wrapper. Form the geodesic continuous $1$-simplex with lift endpoints $a,b$, convert it to a Mathlib singular $1$-simplex, then take the free-module generator of that simplex. No further proof obligations.
why it matters
This is the free $C_1$ avatar of a geodesic edge used throughout the generation and comparison half of the circle homology story. Downstream it identifies $n$ times the fundamental free cycle with $n\cdot\mathrm{geo}(0,2\pi)$, equates $\mathrm{geo}(0,2\pi)$ with the fundamental free generator, and records that $2\pi\mathbb{Z}$ shifts of both endpoints leave the free chain unchanged.
It also feeds the geodesic winding step (shifting the terminal lift by $m$ turns adds $m$ fundamental loops modulo an explicit $2$-boundary), the fact that a degenerate geodesic bounds a constant $2$-simplex, and the free $2$-boundary of a lift-affine $2$-simplex, which is the composition law $\mathrm{geo}(q,r)-\mathrm{geo}(p,r)+\mathrm{geo}(p,q)$ in free $C_1$. Those pieces assemble the terminal-side correction that closes oriented cyclic families, the remaining generation direction toward $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.