coneTerminalSideLift
plain-language theorem explainer
Explicit continuous real lift of the cone terminal-return side for a path on the circle: the straight-line path in R from the covering lift at the path endpoint back to the lift at the start. Downstream displacement lemmas cite it to show that side has displacement opposite the base path. Continuity is elementary arithmetic of continuous maps on the unit interval.
Claim. For a continuous path $\gamma:I\to S^1$, let $\widetilde{\gamma}:I\to\mathbb{R}$ be its canonical covering lift. Define the continuous real path $\widetilde{\gamma}_{\mathrm{term}}:I\to\mathbb{R}$ by $\widetilde{\gamma}_{\mathrm{term}}(t)=(1-t)\,\widetilde{\gamma}(1)+t\,\widetilde{\gamma}(0)$.
background
The module lifts the path-level winding and displacement invariant of CircleWinding to singular 1-simplices on $S^1$, and proves the chain-level identity that displacement kills boundaries of 2-simplices. That identity, with the generator evaluation on the once-around loop, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
SphereOne is the carrier of Mathlib's TopCat.sphere 1. The upstream pathLift is the canonical continuous lift of a path $\gamma:I\to S^1$ through the trigonometric covering $\mathbb{R}\to S^1$, started at a fixed real preimage of $\gamma(0)$. Path displacement is the difference of that lift at the two endpoints (equivalently $2\pi$ times integer winding).
The cone construction on a path produces singular simplices whose faces include a terminal-return side: a path that runs from the endpoint of $\gamma$ back to its start. This definition supplies an explicit real lift of that side by linear interpolation of the endpoint values of pathLift.
proof idea
Definitional construction, not a theorem. The underlying function is the affine combination $(1-t)\cdot\mathrm{pathLift}(\gamma)(1)+t\cdot\mathrm{pathLift}(\gamma)(0)$. Continuity is discharged by composing continuous subtraction, multiplication, and addition on $\mathbb{R}$ with the continuous subtype projection $I\hookrightarrow\mathbb{R}$ and constant maps (the two endpoint values of the lift).
why it matters
This lift is the witness used by coneTerminalSideLift_lifts, which checks that projecting the real path through the trigonometric covering recovers the path of the cone terminal side. That certificate is then fed to pathDisplacement_coneTerminalSide, whose doc-comment states the geometric fact: the terminal-return side has displacement opposite the base path.
Opposite displacement on the return edge is the bookkeeping step that makes the 2-simplex telescoping work: alternating face displacements cancel, so simplexDisplacement vanishes on boundaries. That kills-boundaries identity is the homology-invariance half of the winding homomorphism on 1-cycles, and with the generator evaluation gives the split injection $\mathbb{Z}\hookrightarrow H_1(S^1;\mathbb{Z})$. The module notes that the converse generation half still needs a simplicial prism or subdivision operator not yet in Mathlib singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.