coneLiftAngle_simplexEdge_zero_of_lift_endpoint_eq
plain-language theorem explainer
On the δ₀ face of a 2-simplex cone over a closed path γ on S¹, if the real lift of γ has equal endpoints (zero winding), the lifted cone angle is constantly the common endpoint value. Anyone building the zero-winding cone filler or checking face restrictions of the cone cites this. The proof unfolds the cone formula, identifies the barycentric coordinates on that edge, and case-splits on whether the parameter is the apex.
Claim. Let $\gamma:I\to S^1$ be continuous and suppose its canonical real lift $\widetilde{\gamma}$ satisfies $\widetilde{\gamma}(1)=\widetilde{\gamma}(0)$. Then for every $t\in I$, the lifted cone angle of $\gamma$ evaluated on the $\delta_0$ edge of the standard $2$-simplex at parameter $t$ equals $\widetilde{\gamma}(0)$.
background
This module lifts the path-level winding/displacement invariant on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. That identity is the chain-level reason winding descends to a homology invariant and supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The cone construction fills a closed zero-winding edge by a singular $2$-simplex. The real lifted angle is $\mathrm{coneLiftAngle}(\gamma,x)=(1-x_2),\widetilde{\gamma}(\mathrm{coneBaseParam}(x))+x_2,\widetilde{\gamma}(0)$, radial contraction of the lifted edge toward the apex value. The base parameter is the normalized barycentric coordinate along $v_0\to v_1$ away from the apex $v_2$, and is set to $0$ at the apex.
The $\delta_0$ face map sends a $1$-simplex into $\Delta^2$ so that coordinate $x_2$ is the terminal barycentric coordinate of $\Delta^1$. Upstream, on that face away from the apex the base parameter is identically $1$, so the cone formula samples the terminal endpoint of the lifted edge.
proof idea
Unfold the cone-angle definition. On the $\delta_0$ edge at parameter $t$, the third barycentric coordinate equals $t$ (via the edge embedding, the face-map coordinate identity, and the interval-to-simplex coordinate). Rewrite the formula with that substitution.
Case $t=1$: the point is the apex; the base-parameter convention and simplification give the constant value $\widetilde{\gamma}(0)$.
Case $t\neq 1$: the point is not the apex, so the face-map base-parameter lemma forces the base parameter to be $1$. Substitute, apply the hypothesis $\widetilde{\gamma}(1)=\widetilde{\gamma}(0)$, and simplify the resulting convex combination by ring.
why it matters
This is a face-restriction lemma for the lifted cone filler used to realize zero-winding closed edges as boundaries in the singular chain complex of $S^1$. Its sole downstream consumer is the corresponding statement for the projected circle-valued cone point: once the lifted angle is constant on $\delta_0$, the covering projection yields a constant map equal to $\gamma(0)$ on that face.
In the module's program, such face constancy is part of verifying that the cone is a genuine singular $2$-simplex whose boundary recovers the original closed edge (up to orientation), feeding the kills-boundaries identity and the winding homomorphism on $1$-cycles. Continuity of the cone at the apex remains the stated next frontier; this lemma only treats the $\delta_0$ edge under the lifted endpoint hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.