coneLiftAngle_faceMap_zero
plain-language theorem explainer
On the zeroth face of the standard 2-simplex, the cone lift angle of a path on the circle reduces to the linear join from the terminal real lift back to the initial lift. Anyone checking face restrictions of the zero-winding cone filler cites this identity. The proof unfolds the cone formula, substitutes the face coordinate, and case-splits on whether the sample hits the apex.
Claim. For every continuous path $\gamma:I\to S^1$ and every point $x$ of the standard $1$-simplex $\Delta^1$, the cone lift angle of $\gamma$ at $\delta_0(x)\in\Delta^2$ equals $(1-x_1)\widetilde{\gamma}(1)+x_1\widetilde{\gamma}(0)$, where $\widetilde{\gamma}:I\to\mathbb{R}$ is the canonical continuous real lift of $\gamma$ and $\delta_0:\Delta^1\to\Delta^2$ is the zeroth coface embedding.
background
The module lifts the path-level winding/displacement invariant on $S^1$ to singular simplices and proves the kills-boundaries identity: for every singular $2$-simplex $F$, $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$. Together with the generator evaluation on the once-around loop, that yields the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The cone filler for a closed edge uses the real lifted angle $(1-x_2)\widetilde{\gamma}(\mathrm{coneBaseParam},x)+x_2\widetilde{\gamma}(0)$, where the barycentric base parameter is $x_1/(1-x_2)$ away from the apex $x_2=1$ (and $0$ at the apex). Face maps are the affine coface embeddings $\Delta^1\to\Delta^2$.
On $\delta_0$, the third barycentric coordinate becomes $x_1$. Away from the apex the base parameter collapses to $1$, so the cone formula specialises to the terminal-return side joining $\widetilde{\gamma}(1)$ linearly back to $\widetilde{\gamma}(0)$.
proof idea
Unfold the cone lift angle. Rewrite using the coordinate identity that the second barycentric coordinate of $\delta_0(x)$ equals $x_1$. Case-split on $x_1=1$.
When $x_1=1$, both sides collapse by direct simplification (the prefactor $1-x_1$ vanishes). When $x_1\neq 1$, apply the lemma that the cone base parameter on $\delta_0$ equals the real number $1$ away from the apex, promote that to an equality in the unit interval $I$, substitute into the unfolded formula, and simplify.
why it matters
This is the angle-level $\delta_0$ face restriction needed before projecting back to $S^1$. Its sole recorded parent is the pointwise circle identity that the cone map on $\delta_0$ equals the terminal-return side path (obtained by rewriting through this formula and unfolding the circle-point constructors).
That parent is part of verifying that the cone filler has the correct boundary faces, which supports the zero-winding cone used in the $2$-simplex telescoping argument for the kills-boundaries theorem on singular displacement. In the foundation stack this is pure singular homology of $S^1$: the winding homomorphism on $1$-cycles is the topological input that later underwrites discrete covering and octave arguments, but no RS constants or forcing-chain steps appear in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.