coneCirclePoint_faceMap_zero
plain-language theorem explainer
Pointwise, the δ₀ face of the cone over a path γ : I → S¹ equals the terminal-return side of that cone. Anyone packaging the cone as a continuous singular 2-simplex cites this to name open-edge faces before side terms cancel in a prism. The proof unfolds both sides and rewrites by the lifted-angle face formula on δ₀.
Claim. For every continuous path $\gamma : I \to S^1$ and every point $x$ of the standard $1$-simplex $\Delta^1$, the pointwise cone of $\gamma$ evaluated at the image of $x$ under the face map $\delta_0 : \Delta^1 \to \Delta^2$ equals the terminal-return side of the cone at $x$.
background
This 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$, the alternating face sum of displacements vanishes. Together with the generator evaluation, that yields the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The pointwise cone sends a path $\gamma$ and a point of $\Delta^2$ to $S^1$ by projecting a lifted cone angle through the trigonometric cover. The face map $\delta_0$ is the affine embedding $\Delta^1\to\Delta^2$ induced by the $0$-th coface. The terminal-return side is the continuous $1$-simplex that linearly joins the terminal lift of $\gamma$ back to its initial lift and projects to the circle.
Upstream, the lifted-angle identity already records that the cone angle on $\delta_0$ is exactly that linear join: $(1-x_1)\cdot\mathrm{pathLift}(\gamma)(1)+x_1\cdot\mathrm{pathLift}(\gamma)(0)$.
proof idea
Short term-mode reduction. Unfold the pointwise cone and the terminal-return side; both become the trigonometric cover applied to an angle expression. Rewrite the left-hand angle by the upstream face formula for the lifted cone angle on $\delta_0$, then close by reflexivity. No continuity or endpoint-matching hypotheses are needed at this pointwise stage.
why it matters
Directly feeds the continuous packaging theorem that identifies the $\delta_0$ face of the continuous cone with the terminal-return side. That open-edge face formula is required before side terms cancel in a multi-edge prism, the route toward the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (every $1$-cycle homologous to an integer multiple of the fundamental cycle). The module already has kills-boundaries; this lemma supports the prism/subdivision side that Mathlib singular homology does not yet supply. Pure topological foundation for the winding homomorphism; not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.