coneCircleMapOfContinuous_face_two_path
plain-language theorem explainer
The δ₂ face of the continuous singular 2-simplex cone over a path γ : I → S¹ is exactly the singular 1-simplex of γ. Anyone assembling the cone boundary shell in singular chains cites this identity. The proof is a pointwise extensionality reduction to the already-proved face restriction of the pointwise cone.
Claim. Let $\gamma : I \to S^1$ be continuous, and suppose the pointwise cone map $x \mapsto \mathrm{coneCirclePoint}(\gamma,x)$ on the standard $2$-simplex is continuous. Then the face $\delta_2$ of the packaged singular $2$-simplex cone equals the singular $1$-simplex obtained by reparameterizing $\gamma$ from $\Delta^1$.
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, with the generator sending the once-around loop to $1$, gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Here $S^1$ is the carrier of TopCat.sphere 1. A singular $2$-simplex is a continuous map $\Delta^2\to S^1$; its $i$-th face is composition with the affine face map $\delta_i:\Delta^1\to\Delta^2$. The pointwise cone coneCirclePoint $\gamma$ projects a lifted cone angle through the trigonometric cover; packaging it as a singular $2$-simplex requires a continuity hypothesis at the apex (coneCircleMapOfContinuous). The companion oneSimplexOfPath turns a path $I\to S^1$ into a singular $1$-simplex via the standard homeomorphism $\Delta^1\simeq I$.
Upstream, coneCirclePoint_faceMap_two already states the same equality at the level of bare functions on $\Delta^1$, before continuity packaging.
proof idea
Term-mode, three steps. First ext x reduces equality of continuous maps (singular $1$-simplices) to pointwise equality on $\Delta^1$. Unfolding face and coneCircleMapOfContinuous rewrites the left-hand side as the pointwise cone evaluated on the geometric face map $\delta_2$. The resulting identity is exactly coneCirclePoint_faceMap_two, which is applied directly. No new analysis: continuity of the cone is only used to form the packaged simplex, not in the face computation.
why it matters
This is the base-face brick in the path-parametric cone boundary. Downstream, singularTwoBoundaryFree_freeMk_coneSingularTwoSimplexOfPath uses it to identify the free singular boundary of the cone over $\gamma$ as
terminal-return side minus constant apex side plus the path edge itself. That shell is the primitive finite-prism generator needed before multi-edge cancellation in the subdivision/prism operator that would finish surjectivity of the integer comparison map on $H_1(S^1)$.
In the module narrative, the kills-boundaries identity already gives injectivity of winding on homology; the missing generation half needs exactly these cone faces so that every $1$-cycle can be reduced, via prisms, to an integer multiple of the fundamental loop. The declaration closes the $\delta_2$ face of that cone under the continuity hypothesis already isolated by coneCircleMapOfContinuous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.