coneTerminalSide
plain-language theorem explainer
The terminal-return side of the cone over a path γ on S¹ is the singular 1-simplex that linearly interpolates, in the covering angle, from the lifted endpoint of γ back to its lifted start and projects by the trigonometric chart. Cone-face and prism identities for the winding-kills-boundaries argument cite this edge. Continuity is composition of the barycentric coordinate with the continuous circle parametrization.
Claim. For a continuous path $\gamma:I\to S^1$, the terminal-return side is the singular $1$-simplex $\Delta^1\to S^1$ sending $x$ to the trigonometric point at angle $(1-x_1)\widetilde{\gamma}(1)+x_1\widetilde{\gamma}(0)$, where $\widetilde{\gamma}$ is the canonical continuous real lift of $\gamma$.
background
This module lifts the path-level winding/displacement invariant of the circle covering to singular simplices of $S^1$, and proves that displacement vanishes on boundaries: for every singular $2$-simplex the alternating face sum of displacements is zero. That identity is the chain-level half of the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$.
A singular $1$-simplex here is a continuous map $\Delta^1=\mathrm{stdSimplex},\mathbb{R}(\mathrm{Fin},2)\to S^1$. The covering lift of a path $\gamma$ is the unique continuous real lift starting at the canonical base lift; the trigonometric chart sends a real angle to the corresponding point of the exact $\mathrm{TopCat}$ sphere object and is continuous.
The cone over $\gamma$ needs three boundary edges. The terminal-return side is the open edge that runs, in covering coordinates, from the lifted end of $\gamma$ back to the lifted start: the geodesic return that closes the cone prism.
proof idea
Definitional construction, not a derived theorem. The underlying map on $\Delta^1$ is the composition of the affine interpolation $(1-x_1)\widetilde{\gamma}(1)+x_1\widetilde{\gamma}(0)$ with the trigonometric chart. Continuity is proved by composing continuity of the chart with continuity of the barycentric coordinate $x\mapsto x_1$ (subtype projection then continuous_apply) and the elementary continuous arithmetic of subtraction, multiplication by constants, and addition.
why it matters
This edge is the $\delta_0$ face of the cone map: the face-zero theorems identify the cone's open face with the terminal-return side, which is the open-edge formula needed before side terms cancel in a multi-edge prism. Equality with the geodesic $1$-simplex from lifted end to lifted start makes geodesic calculus available. When the lift endpoints agree (equivalently, when simplex winding vanishes), the side collapses to the constant apex edge, so zero-winding cones contribute no residual boundary. Downstream oriented cyclic family terms and the kills-boundaries telescoping therefore rest on this concrete return edge. In the module's larger program it 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.