continuousAt_coneCirclePoint_of_coord_two_ne_one
plain-language theorem explainer
Away from the apex of the standard 2-simplex, the pointwise S¹-cone of a continuous path is continuous. Anyone packaging that cone as a continuous map Δ² → S¹ cites this local fact. The proof is a one-line composition: non-apex continuity of the lifted cone angle, then the continuous trigonometric covering of the circle.
Claim. Let $\gamma : I \to S^1$ be continuous and let $x$ lie in the standard $2$-simplex $\Delta^2 \subset \mathbb{R}^3$. If the third barycentric coordinate satisfies $x_2 \neq 1$, then the pointwise cone map $x \mapsto \mathrm{trig}(\mathrm{coneLiftAngle}(\gamma,x))$ is continuous at $x$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries of $2$-simplices, the chain-level fact behind a left inverse $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$.
Here $S^1$ is the carrier of Mathlib's TopCat.sphere 1. The trigonometric covering $\mathrm{trigCirclePoint}:\mathbb{R}\to S^1$ is continuous. The pointwise cone $\mathrm{coneCirclePoint}(\gamma)$ sends a barycentric point $x\in\Delta^2$ to $\mathrm{trigCirclePoint}$ of a lifted cone angle built from $\gamma$; it is not yet a packaged continuous map.
The apex of $\Delta^2$ is the vertex where the third coordinate equals $1$. Away from that vertex the lifted angle is already known to be continuous at $x$; this lemma pushes that continuity through the covering.
proof idea
Unfold the definition of the pointwise cone (composition of the lifted cone angle with the trigonometric covering). Apply continuity-at of the covering map, then compose with the already-proved non-apex continuity of the lifted cone angle at the same $x$. Term-mode, no further case splits.
why it matters
Feeds the global continuity theorem for the pointwise cone: that result cases on whether $x_2=1$, handles the apex by a squeeze argument, and invokes this lemma on the complementary open set. Closing continuity of the cone is the analytic packaging step needed before the cone can serve as a continuous singular $2$-simplex in the winding/homology argument of the module (the kills-boundaries identity and the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). No Recognition forcing-chain landmark is touched directly; the work is pure foundational topology supporting the circle winding invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.