geodesicFreeChain_shift
plain-language theorem explainer
Shifting both lift endpoints of a geodesic free 1-chain by the same integer multiple of 2π leaves the chain unchanged. Workers building the singular-chain winding map on S¹ cite this when normalizing lifts into a common fundamental domain. The proof unfolds the free-chain constructor and rewrites by the corresponding one-simplex shift identity.
Claim. For all $a,b\in\mathbb{R}$ and every $m\in\mathbb{Z}$, the free singular $1$-chain generated by the lift-linear geodesic from $a+2\pi m$ to $b+2\pi m$ equals the free singular $1$-chain generated by the geodesic from $a$ to $b$.
background
This module lifts the path-level winding and displacement invariant of the circle to singular simplices of $S^1$, and proves that displacement kills boundaries: the alternating face sum of any singular $2$-simplex has vanishing displacement. That identity, together with evaluation $1$ on the once-around generator, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A geodesic free chain is the free $C_1$ generator on the singular $1$-simplex obtained by projecting the affine lift path from real endpoint $a$ to $b$ down to the circle. Because the covering map $\mathbb{R}\to S^1$ identifies points differing by $2\pi\mathbb{Z}$, the projected edge depends only on the classes of the endpoints.
The upstream one-simplex shift theorem records exactly that geometric fact: translating both lift endpoints by $m\cdot 2\pi$ leaves the singular geodesic map unchanged. The free-chain object is just the free-module generator on that map, so the same invariance passes to chains.
proof idea
One-line reduction. Unfold the definition of the free geodesic chain (the free $C_1$ generator on the singular geodesic one-simplex). Rewrite by the already-proved one-simplex shift identity, which equates the geodesic maps after a common $2\pi m$ translation of both endpoints. Equality of the underlying singular simplices yields equality of the free chains.
why it matters
The immediate consumer is the one-turn geodesic boundary identity: the free boundary of the lift-affine $2$-simplex on $(0,2\pi,z+2\pi)$ expands as $\mathrm{geo}(0,z)-\mathrm{geo}(0,z+2\pi)+\mathrm{geo}(0,2\pi)$, and the proof folds the side $(2\pi,z+2\pi)$ onto $(0,z)$ by this shift invariance. That linear step is part of the chain-level computation that winding kills boundaries and that the winding homomorphism is a left inverse to the fundamental class, i.e. the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
In the broader Recognition foundation this is bookkeeping for the circle's first homology, not a forcing-chain landmark (T5–T8). It closes a normalization gap so later singular-chain arguments can fix lifts without tracking covering ambiguity. The generation/surjectivity half of the integer comparison still needs a prism or subdivision operator that Mathlib singular homology does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.