geodesicOneSimplex_shift
plain-language theorem explainer
Translating both lift endpoints of a geodesic singular 1-simplex by the same integer multiple of 2π leaves the simplex unchanged as a map Δ¹ → S¹. Anyone building free chains or winding classes from lift data cites this deck-invariance. The proof is pointwise: affine combination absorbs the common shift, then the covering fiber criterion identifies the points on S¹.
Claim. For all $a,b\in\mathbb{R}$ and $m\in\mathbb{Z}$, the geodesic singular $1$-simplex with lift endpoints $a+2\pi m$ and $b+2\pi m$ equals the geodesic singular $1$-simplex with endpoints $a$ and $b$: both are the same continuous map $\Delta^1\to S^1$.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A geodesic singular $1$-simplex is the projection of the straight line in the universal cover $\mathbb{R}\to S^1$: at $x\in\Delta^1$ it evaluates $\mathrm{trigCirclePoint}$ on the affine combination $(1-x_1)a+x_1 b$. Here $\mathrm{trigCirclePoint}$ is the once-around trigonometric parametrization into the exact TopCat.sphere 1 object.
The key covering fact is the fiber criterion: $\mathrm{trigCirclePoint},a=\mathrm{trigCirclePoint},b$ iff $a-b\in 2\pi\mathbb{Z}$, i.e. the deck group of the cover.
proof idea
Pointwise extensionality on $\Delta^1$. After unfolding the geodesic evaluation, the affine combination of the shifted endpoints equals the unshifted combination plus the common term $m\cdot 2\pi$ (ring). The covering fiber theorem then supplies equality of the two $\mathrm{trigCirclePoint}$ values, witnessed by that same integer $m$.
why it matters
Deck-invariance of geodesic $1$-simplices is the atomic step for free-chain shift invariance: the downstream result that a $2\pi\mathbb{Z}$ shift of both lift endpoints leaves the geodesic free chain unchanged is a one-line unfold-and-rewrite through this theorem.
In the module's program, geodesic simplices are the concrete generators whose displacements realize winding. Without shift invariance, lift choices would pollute chain-level classes. Together with the kills-boundaries identity and the fundamental-loop normalization, this supports the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation/surjectivity half still needs a simplicial prism operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.