coneCirclePoint_simplexEdge_one
plain-language theorem explainer
On the δ₁ edge of the standard 2-simplex, the pointwise S¹ cone of a path γ is constantly the path's starting point γ(0). Anyone building the cone homotopy that proves winding kills boundaries on singular 2-simplices cites this edge evaluation. The proof unfolds the cone, reduces the lifted angle to the constant initial lift, and projects via the covering identity.
Claim. For every continuous path $\gamma : I \to S^1$ and every $t \in I$, the pointwise cone of $\gamma$ evaluated on the geometric $\delta_1$-edge of $\Delta^2$ equals the basepoint of the path: $\mathrm{cone}(\gamma)(\delta_1(t)) = \gamma(0)$.
background
The module lifts path-level winding on $S^1$ to singular simplices 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 geometric edge map sends the unit interval into $\Delta^2$ along the $i$-th face. The pointwise cone of a path $\gamma$ is obtained by lifting $\gamma$ to an angle path on $\mathbb{R}$, forming a linear cone angle on $\Delta^2$, and projecting back through the trigonometric covering $\mathbb{R} \to S^1$. Continuity of that cone at the apex is still open; only the pointwise map is used here.
Upstream, the lifted cone angle is already known to be constantly the initial lift value on the $\delta_1$ edge. The covering identity says projecting the path lift recovers $\gamma$ pointwise.
proof idea
Unfold the pointwise cone definition (trig cover of the lifted cone angle). Rewrite the angle on the $\delta_1$ edge via the upstream constancy lemma, which replaces it by the constant initial lift $\mathrm{pathLift},\gamma,0$. Apply the covering identity $\mathrm{trig}\circ\mathrm{pathLift},\gamma = \gamma$ at time $0$ (via congruence of functions) to obtain $\gamma(0)$. Three short steps; no new analysis.
why it matters
The kills-boundaries theorem for singular 2-simplices needs a cone (or prism) homotopy on $\Delta^2$ that collapses two boundary edges onto the third. Constancy of the projected cone on the $\delta_1$ side is the edge evaluation that makes that homotopy fix the correct face values and therefore telescope displacements.
Together with the once-around generator sending winding to $1$, this infrastructure supplies the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. In the Recognition forcing chain the circle and its winding control the eight-tick octave (T7) and the topological side of the recognition calculus; a clean singular-homology winding map is the algebraic home for that period.
No downstream consumers are wired yet in the graph. The immediate parent target is the 2-simplex telescoping identity in this module; the longer open piece remains generation of $H_1$ (surjectivity), which needs a simplicial prism or subdivision operator Mathlib does not yet expose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.