coneCirclePoint_simplexEdge_two
plain-language theorem explainer
On the base edge of the standard 2-simplex, the pointwise circle cone of a path γ recovers γ itself. Anyone building the cone homotopy that proves winding kills boundaries on singular 2-simplices will cite this face restriction. The proof unfolds the cone, reduces the lifted angle on that edge to the path lift, then applies the covering-map lift identity.
Claim. For every continuous path $\gamma : I \to S^1$ and every $t \in I$, the pointwise cone of $\gamma$ evaluated on the base edge of $\Delta^2$ (the edge selected by the face map indexed by $2 \in \mathrm{Fin}\,3$) equals $\gamma(t)$: $\mathrm{cone}(\gamma)(\mathrm{edge}_2(t)) = \gamma(t)$.
background
This module lifts the path-level winding and displacement invariant of CircleWinding to singular simplices of $S^1$, and proves that displacement vanishes on boundaries of singular 2-simplices. The geometric edges of the standard 2-simplex $\Delta^2$ are the continuous maps $\mathrm{edge}_i : I \to \Delta^2$ obtained by composing the $i$-th face map with the standard interval-to-1-simplex reparameterization.
The pointwise cone sends a path $\gamma$ and a point $x \in \Delta^2$ to the image under the trigonometric covering map of a lifted cone angle built from the path lift of $\gamma$. The covering identity states that projecting the path lift recovers $\gamma$ pointwise: $\mathrm{trig} \circ \mathrm{pathLift}(\gamma) = \gamma$. An upstream lemma already records that on the base edge the lifted cone angle equals the path lift itself.
proof idea
Term-mode, three steps. Unfold the pointwise cone definition so the goal is equality of trigonometric projections of angles. Rewrite the lifted cone angle on $\mathrm{edge}_2(t)$ via the base-edge angle lemma, replacing it by $\mathrm{pathLift}(\gamma)(t)$. Finish by applying function congruence to the covering lift identity $\mathrm{trig} \circ \mathrm{pathLift}(\gamma) = \gamma$ at the point $t$.
why it matters
The cone is the geometric device behind the 2-simplex telescoping that proves displacement kills boundaries: the walk along two faces is homotopic rel endpoints, inside the convex (hence simply connected) standard 2-simplex, to the direct third edge. Restricting the cone to the base edge is the face identity that pins the cone to the original path, so the pushed homotopy really starts from $\gamma$.
Together with path-winding of the fundamental loop equaling 1, the kills-boundaries identity supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. No downstream consumers are wired yet; this lemma is local infrastructure for packaging the cone as a continuous map and closing the boundary identity. Continuity of the cone at the apex remains an open frontier noted in the cone definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.