coneTerminalSide_eq_geodesic
plain-language theorem explainer
The terminal-return side of the cone over a path on S¹ equals the geodesic singular 1-simplex from the path's terminal lift value back to its initial lift value. Anyone building the bounding 2-chain for oriented cyclic families cites this identification. The proof is pure definitional equality: both sides expand to the same affine lift projected by the trigonometric covering.
Claim. For every continuous path $\gamma : I \to S^1$, the terminal-return side of the cone over $\gamma$ equals the geodesic singular $1$-simplex joining the terminal value of the canonical real lift of $\gamma$ to its initial value.
background
This module lifts the path-level winding/displacement invariant on $S^1$ to singular simplices and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
The canonical lift of a path $\gamma$ is the continuous real-valued path obtained from the trigonometric covering $\mathbb{R} \to S^1$, started at a fixed lift of $\gamma(0)$. A geodesic singular $1$-simplex from lift values $a$ to $b$ is the projection of the straight-line segment $(1-t)a + tb$ under that covering. The terminal-return side of the cone over $\gamma$ is defined by the same formula with $a = \mathrm{lift}(\gamma)(1)$ and $b = \mathrm{lift}(\gamma)(0)$: it closes the cone by returning from the terminal lift angle to the initial one.
proof idea
One-line definitional equality (rfl). Unfolding the terminal-return side yields $\mathrm{trig}((1-x_1)\cdot\mathrm{lift}(\gamma)(1) + x_1\cdot\mathrm{lift}(\gamma)(0))$. Unfolding the geodesic $1$-simplex at those same endpoints yields the identical map. No lemmas are applied.
why it matters
Feeds the parent theorem that the terminal-side correction target for oriented cyclic families is closed unconditionally. That result needs every terminal-return side to be a geodesic from the terminal lift of one edge to the initial lift of the next, so that cyclic connectivity of lifts (agreement mod $2\pi\mathbb{Z}$) produces integer winding steps and an explicit bounding $2$-chain from lift-affine cones and winding-step prisms.
In the module's larger program this is bookkeeping on the cone construction used to compare path displacement with simplicial displacement. It does not itself compute $H_1$, but it removes an equality obligation before the generation/correction argument can run. Landmark context: the winding homomorphism left-inverse to the fundamental class on $S^1$, the chain-level kills-boundaries identity, and the still-open generation half that needs a simplicial prism/subdivision operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.