continuousAt_coneCirclePoint_apex
plain-language theorem explainer
The pointwise cone map from the standard 2-simplex into S¹ is continuous at the apex vertex. Anyone assembling a continuous cone filler for a closed edge on the circle cites this. The proof identifies the apex value with the path basepoint and reduces to the already-proved squeeze/tendsto lemma at that vertex.
Claim. For every continuous path $\gamma : I \to S^1$, the pointwise cone $x \mapsto \mathrm{trig}(\mathrm{coneLiftAngle}(\gamma,x))$ from the standard $2$-simplex $\Delta^2$ into $S^1$ is continuous at the apex vertex $v_2 = (0,0,1)$.
background
This module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. That identity is the chain-level half of the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$.
The cone construction fills a closed edge $\gamma$ over the apex of $\Delta^2$. The barycentric base parameter normalizes the base edge away from the apex and is set to $0$ at the apex. The lifted cone angle multiplies the lifted path angle by the complementary height $1-x_2$, so the angle collapses to the start value as one approaches the apex. Projecting through the trigonometric covering map yields the pointwise circle-valued cone.
Upstream, the covering lift of $\gamma$ satisfies $\mathrm{trig}\circ\mathrm{pathLift}(\gamma)=\gamma$, and a separate tendsto lemma already shows the cone tends to the basepoint at the apex.
proof idea
Rewrite continuity-at as a filter tendsto statement. Compute the cone value at the apex vertex by unfolding the cone angle: the height factor is $0$, so the expression collapses to $\mathrm{trig}(\mathrm{pathLift}(\gamma)(0))$. The covering identity then gives exactly $\gamma(0)$. After rewriting the target neighborhood to that of $\gamma(0)$, invoke the prior tendsto-to-apex lemma for the same cone.
why it matters
This is the singular analytic step in packaging the pointwise cone as a genuine continuous map $\Delta^2\to S^1$. Downstream, global continuity of the cone is obtained by case-splitting on the apex coordinate: at the apex one applies this theorem; away from it one uses ordinary coordinate continuity of the lifted angle composed with the covering map.
A continuous cone filler supplies the nullhomotopy needed in the $2$-simplex telescoping argument that displacement kills boundaries. That vanishing, together with the fact that winding sends the once-around generator to $1$, yields the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. No Recognition forcing-chain landmark (T5–T8, RCL) is touched here; the result is pure foundational topology supporting the winding invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.