coneTerminalSide_eq_constantOneSimplex_of_lift_endpoint_eq
plain-language theorem explainer
When a path on S¹ has equal lifted endpoints, the terminal-return side of its cone equals the constant singular edge at the path's basepoint. Homology and winding arguments cite this to collapse cone edges under zero displacement. The proof is pointwise: substitute equal lifts, cancel the convex combination by ring, and apply the covering lift identity.
Claim. Let $\gamma : I \to S^1$ be continuous. If the canonical real lift satisfies $\widetilde{\gamma}(1) = \widetilde{\gamma}(0)$, then the terminal-return cone edge of $\gamma$ equals the constant singular $1$-simplex at $\gamma(0)$.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$ and proves that displacement kills boundaries, the chain-level fact behind the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
The covering map is the trigonometric parametrization: trigCirclePoint sends a real angle to a point of the exact TopCat.sphere 1. For a path $\gamma$ on the circle, pathLift is the canonical continuous real lift starting at a fixed branch; pathLift_lifts says $\mathrm{trigCirclePoint} \circ \widetilde{\gamma} = \gamma$.
coneTerminalSide $\gamma$ is the singular edge on $\Delta^1$ that linearly interpolates the lifted endpoints in the cover and projects back: $x \mapsto \mathrm{trigCirclePoint}\bigl((1-x_1)\widetilde{\gamma}(1)+x_1\widetilde{\gamma}(0)\bigr)$. constantOneSimplex $p$ is the constant map $\Delta^1 \to S^1$ at $p$.
proof idea
Pointwise extensionality on $\Delta^1$. Unfold the cone side to $\mathrm{trigCirclePoint}$ of the convex combination of the two lifted endpoints. Rewrite with the hypothesis $\widetilde{\gamma}(1)=\widetilde{\gamma}(0)$, so both coefficients multiply the same real. A one-line ring identity collapses $(1-x_1)a+x_1 a$ to $a$. The covering identity pathLift_lifts then gives $\mathrm{trigCirclePoint}(\widetilde{\gamma}(0))=\gamma(0)$, matching the constant simplex.
why it matters
Feeds the parent theorem coneTerminalSide_eq_constantOneSimplex_of_simplexWinding_zero: zero simplex winding forces equal lifted endpoints, hence the cone's terminal-return side is the constant apex edge. That collapse is the geometric content of "zero winding means the return edge is null" in the cone construction used for the winding-kills-boundaries identity.
In the module's program, simplexDisplacement_boundary shows the alternating face sum of displacement on every singular $2$-simplex vanishes (telescoping via convex homotopy in $\Delta^2$). Together with the fundamental loop mapping to winding $1$, this supplies the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The present lemma is a local algebraic step inside that cone/edge bookkeeping, not a forcing-chain (T0–T8) landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.