continuous_coneCirclePoint
plain-language theorem explainer
For any continuous path γ on the circle, the pointwise cone map from the standard 2-simplex into S¹ is continuous. Homology and singular-simplex arguments that build a 2-simplex by coning a path cite this packaging step. Continuity is reduced to pointwise continuous-at, then split into the apex (squeeze) case and the ordinary non-apex coordinate case.
Claim. Let $\gamma : I \to S^1$ be continuous. The pointwise cone map $c_\gamma : \Delta^2 \to S^1$, obtained by projecting the lifted cone angle through the trigonometric circle cover, is continuous.
background
The module lifts path-level winding and displacement on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular 2-simplex $F$, the alternating face sum of displacements vanishes. That identity, with the fundamental loop sending to winding 1, gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Here $S^1$ is the carrier of Mathlib's TopCat.sphere 1. The pointwise cone coneCirclePoint γ sends $x\in\Delta^2$ to the circle point of the lifted cone angle of γ at $x$. Continuity away from the apex is ordinary composition with the covering map; the apex $v_2$ (where the third barycentric coordinate equals 1) is the only singular analytic point and was handled by a squeeze argument.
The identity that $x_2=1$ forces $x=v_2$ on the standard 2-simplex glues the two local continuity statements into a global continuous map $\Delta^2\to S^1$.
proof idea
Rewrite global continuity as continuous-at every point. Fix $x\in\Delta^2$ and case on whether the third barycentric coordinate equals 1.
If $x_2=1$, the simplex identity forces $x$ to be the apex vertex $v_2$; apply the apex continuous-at theorem (the squeeze argument).
If $x_2\neq 1$, apply non-apex continuous-at: unfold the cone as the covering map of the lifted angle and compose continuous-at of the covering with continuous-at of the lifted angle off the apex.
No new analysis is done here; the proof only cases and invokes the two local lemmas plus the apex-recognition identity.
why it matters
This closes the analytic packaging gap for the pointwise cone: once continuity is proved, the cone can be promoted to a continuous map and thence to a singular 2-simplex. Downstream, coneSingularTwoSimplexOfPath builds that singular 2-simplex by feeding this continuity witness into the continuous-map constructor. The free-boundary shell theorems for the cone over an arbitrary edge, and the zero-winding specialization that makes the free boundary just the original edge, both depend on that continuous cone. The closed zero-winding edge bounding theorem likewise cites it to remove the last analytic hypothesis from the single-edge cone construction.
In the module's larger program, these cones supply the 2-chains that witness boundaries in the winding-kills-boundaries identity, supporting the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The generation/surjectivity half still needs a simplicial prism or subdivision operator not yet in Mathlib singular homology; this lemma does not touch that open half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.