continuousAt_coneLiftAngle_of_coord_two_ne_one
plain-language theorem explainer
Away from the apex of the standard 2-simplex, the real-valued lifted cone angle built from a continuous path on S¹ is continuous. Anyone constructing a continuous cone filler for a closed edge (toward the kills-boundaries identity) cites this. The proof unfolds the angle formula and chains continuity of the barycentric base parameter, the covering path lift, and coordinate arithmetic.
Claim. Let $\gamma:I\to S^1$ be continuous and let $x\in\Delta^2=\mathrm{stdSimplex}\,\mathbb{R}\,(\mathrm{Fin}\,3)$. If the apex barycentric coordinate satisfies $x_2\neq 1$, then the lifted cone angle of $\gamma$ is continuous at $x$.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices on $S^1$ and proves that displacement kills boundaries: for every singular 2-simplex $F$, the alternating face sum of displacements vanishes. That identity is the chain-level fact behind the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The cone construction fills a closed edge by coning over the apex $v_2$ of $\Delta^2$. The barycentric base parameter sends $x$ (away from the apex) to the normalized base coordinate $x_1/(1-x_2)\in I$, and to $0$ at the apex. The path lift is the canonical continuous real lift of $\gamma$ through the trigonometric covering of $S^1$. The lifted cone angle blends that lifted path against the height coordinate $x_2$ so the filler can later be continuous at the apex as well.
The local claim is ordinary pointwise continuity of that angle map on the open set ${x_2\neq 1}$.
proof idea
Unfold the lifted cone angle. Continuity of the base parameter at $x$ is the sibling lemma for $x_2\neq 1$. Compose with continuity of the path lift of $\gamma$ to get continuity of $y\mapsto\mathrm{pathLift}(\gamma)(\mathrm{coneBaseParam},y)$. The second barycentric coordinate $y\mapsto y_2$ is continuous as a subtype projection. The angle formula is built from subtraction, multiplication, and addition of these pieces against constants; close by the corresponding continuous-at rules.
why it matters
Parent use is continuity of the cone circle point away from the apex: that theorem composes this result with the continuous trigonometric covering map. Together they supply the non-apex half of a continuous cone filler for a closed edge on $S^1$.
That filler is scaffolding for the 2-simplex telescoping argument in the module doc: the boundary walk along two edges is homotopic rel endpoints inside convex $\Delta^2$ to the direct edge, and pushing the homotopy through $F$ with path-displacement additivity and homotopy invariance yields the kills-boundaries identity. With the fundamental loop sent to winding one, this is 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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.