coneLiftAngle_faceMap_zero_of_lift_endpoint_eq
plain-language theorem explainer
On the side face δ₀ of the standard 2-simplex, the real cone lift angle of a path γ : I → S¹ is constantly equal to the initial lift value whenever the path lift closes (equal endpoints). Anyone building the zero-winding cone filler or the side-face restrictions for the kills-boundaries identity cites this. The proof unfolds the cone formula, splits on the apex coordinate, and uses the face-parameter identity that the base parameter is 1 off the apex together with endpoint equality.
Claim. Let $\gamma : I \to S^1$ be continuous and suppose its canonical real lift satisfies $\widetilde{\gamma}(1) = \widetilde{\gamma}(0)$. Then for every point $x$ of the standard $1$-simplex, the cone lift angle of $\gamma$ evaluated on the face map $\delta_0(x)$ equals $\widetilde{\gamma}(0)$.
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$ and proves that displacement kills boundaries: for every singular $2$-simplex $F$, $\mathrm{disp}(\delta_0 F) - \mathrm{disp}(\delta_1 F) + \mathrm{disp}(\delta_2 F) = 0$. That identity is the chain-level half of the split injection $H_1(S^1;\mathbb{Z}) \hookrightarrow \mathbb{Z}$.
The cone construction fills a closed zero-winding edge over an apex. The real angle used is $\mathrm{coneLiftAngle}(\gamma,x) = (1-x_2),\widetilde{\gamma}(\mathrm{coneBaseParam}(x)) + x_2,\widetilde{\gamma}(0)$, which radially contracts the lifted edge toward the initial lift. The barycentric base parameter is $x_1/(1-x_2)$ off the apex $v_2$ and $0$ at the apex.
On the side face $\delta_0$, away from the apex, an upstream lemma already shows the base parameter is identically $1$, so the formula samples the terminal lift of the edge. The present result packages that with endpoint equality into constancy of the whole lifted angle on $\delta_0$.
proof idea
Unfold the definition of the cone lift angle. A coordinate identity for $\delta_0$ rewrites the apex weight $x_2$ as the second barycentric coordinate of the $1$-simplex point $x$. Case-split on whether that coordinate equals $1$ (the apex of the face).
If it is $1$, simplification collapses the formula to the initial lift. If not, apply the upstream face lemma that the cone base parameter on $\delta_0$ is $1$, coerce that equality back to the unit interval, substitute, and cancel with the hypothesis that the path lift closes; a short ring step finishes.
why it matters
This is the real-angle half of the $\delta_0$ side restriction for the zero-winding cone filler. The immediate parent is the pointwise $S^1$ statement that the cone circle point on $\delta_0$ is constantly $\gamma(0)$ under the same endpoint hypothesis; that parent simply unfolds the circle-point map and rewrites by this theorem.
Together the side-face formulae let the cone restrict correctly on the boundary edges of a $2$-simplex, which is the analytic input to the telescoping argument that simplex displacement kills boundaries. In the broader Recognition foundation this supplies the homology-invariant half of the comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (the generator half still needs a prism/subdivision operator Mathlib does not yet provide). No T0–T8 forcing step is touched directly; the result is pure singular-homology scaffolding for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.